VeriPlan

Christine P. Lee, David Porfirio, Xinyu Jessica Wang, Kevin Chenkai Zhao, and Bilge Mutlu. CHI 2025. Paper

VeriPlan checks an LLM's plan against rules the user confirms, using model checking, and sends any violations back to the user and the LLM. Try it on the patient navigation task from the paper.

The LLM's plans are scripted for this demo. The rule translations are the ones the system presented, and constraint sampling and model checking run live in your browser.

The task: patient navigation

You (P1) are a family counselor preparing a family therapy session. Three family members, P2, P3, and P4, are waiting with you in the waiting room (L1). Hospital safety protocols say you must escort each of them to the counseling room (L2) yourself, one person at a time. Because of ongoing tensions, P2 and P3 cannot be left alone together, and neither can P3 and P4.

Ask the planner: in what order should you move everyone?

Everyone starts in the waiting room L1 and must end in the counseling room L2. P1 escorts one person at a time. P2 and P3, and P3 and P4, cannot be left alone together. L1 waiting room L2 counseling room escort 1 at a time P1 P2 P3 P4 can't be left alone together everyone ends here

1Input Panel
Built with Chainlit
The planning canvas fills in as you work.
Drag to pan. Ctrl + scroll to zoom.