Interactive Labs
Bounded, replayable teaching labs paired with the tutorials. Each one turns an abstract claim into something visible: a witness, a quotient, a bad state, or a compiled controller.
Scope note
These labs use small bounded models for teaching clarity, not full proofs of unrestricted systems. Each harness is a simplified but replayable slice of a tutorial’s formal object, and a demonstrated counterexample shape or search geometry should be read as a concrete witness inside that bounded model, not as a claim of general completeness.
Suggested first path
Start with the Concolic Branch Lab, then move to the Grammar Witness Search Lab, and only then open the Grammar-to-Solver Handoff Lab. Each step adds one new idea on top of the previous one: first path-directed search, then syntax-preserving search, then the hybrid moment where structured search hands off to local solving. Skipping ahead makes the later lab feel like a trick instead of a consequence.
Witness Search Track
Concolic Branch Lab
Concrete run, path condition, branch flip, bounded solve, replay. This is the hands-on companion to Tutorial 35.
Grammar Witness Search Lab
Compare raw-byte search with grammar-guided generation on the same bad-state predicate. This is the companion lab for Tutorial 36.
Grammar-to-Solver Handoff Lab
Watch structured generation stay valid, then hand off to a bounded solver when the remaining obstacle is semantic rather than syntactic.
Witness Space Explorer
See proposal distributions, acceptance regions, and found witnesses move against each other in a bounded search space.
Loop Geometry Track
If the witness-search track is finished, this is the best next stop. Start with the Hybrid Loop Comparison Lab, then move to Galois Loop Lab if the goal is to see how the search space itself can be reshaped.
Hybrid Loop Comparison Lab
Compare direct control with two hybrid loops on the same bounded task and inspect what the hybrid stages are actually buying.
Galois Loop Lab
Watch obligation carving happen over a finite relation universe and see how the quotient changes the repair problem.
Verifier-Compiler Lab
See verifier labels collapse into a smaller symbolic controller, and inspect when that compression is pure and when it is mixed.
Temporal Label Basis Lab
Compare coarse and richer temporal label bases, then see why the stronger basis becomes exact only after the right first carve.
State and Shape Track
For a gentler change of pace, start here with the Vending Machine Explorer. It is the most concrete entry point for states, transitions, and invariants before the later shape tutorials become more abstract.
Vending Machine Explorer
A small live state machine for learning states, transitions, and invariants before the tutorials become more abstract.
Shape Evolution Explorer
Move through shape choices and see how adding clauses changes the reachable system behaviors.
ZenoDEX Shape Pruning Lab
Treat clauses as structural blockers on disaster states and inspect what each strengthening step actually removes.