PathProof

• 

  Inspect a complete decision workflow in one workspace.

• 

  Review grouped findings from exhaustive path analysis.

• 

  Replay the exact counterexample that exposes a missing route.

• 

  Apply a repair, rerun all scenarios, and verify completion.

Inspiration

Small forms and decision trees can look complete while leaving someone stranded. A library member who has not completed training should get a next step, not a dead end. PathProof makes these omissions concrete and explainable.

What it does

PathProof checks every combination of up to eight fixed boolean inputs in a finite workflow. It detects missing routes, overlapping decisions, cycles, and nodes never visited by an unambiguous run. Each execution failure comes with an exact input assignment, node path, and edge path that can be replayed visually.

The included borrowing example starts with six of eight scenarios terminating. A visible repair adds the missing training route; rerunning checks all eight combinations and reaches every node. Users can import or edit declarative JSON, save a validated model locally, and export a Markdown audit containing the entire model and every scenario.

How we built it

React presents a responsive workspace and SVG topology. A separate TypeScript engine validates the model, enumerates boolean assignments, and performs deterministic graph walks. Exactly one matching edge continues execution; zero or multiple matching edges stop with evidence. Repeating a node under fixed inputs identifies a cycle.

Challenges

The key design decision was defining what a result means. PathProof stops at ambiguous decisions instead of inventing edge priority. “Unvisited” is relative to those semantics, and both the UI and exported evidence state that boundary.

Accomplishments

A complete inspect → replay → repair → rerun → export loop works with reproducible evidence. Every visible control was verified on desktop and mobile. The deterministic domain engine has complete test coverage.

What we learned

Exhaustive checks become practical when a model is deliberately small. Counterexamples are more useful than a pass/fail badge, and a correctness claim is meaningful only when its assumptions are visible.

What's next

A visual edge editor and additional classroom examples could make authoring easier. Testing mutable input values or live services would require a different state model.

AI assistance

OpenAI Codex assisted planning, interface design, implementation, tests, debugging, documentation, and demo preparation. Runtime checking is deterministic TypeScript; no AI model is called.

Built With

• ffmpeg
• openai-codex
• playwright
• react
• svg
• testing-library
• typescript
• vite
• vitest