Inspiration:

Thousands of people are denied basic rights by regulations they followed perfectly. A single-day threshold shifts eligibility by one person, yet those thresholds are rarely audited for unintended consequences. We wanted a tool that does what regulators cannot scale to: exhaustively test every edge case of a regulation before it takes effect.

What we built:

Trapdoor pins 8 CFR 274a.13 (Employment Eligibility Verification) as it stood on January 1, 2022, represents it as a typed graph in Jac with five clauses linked by Precedes edges, and seeds seven real applicant profiles that exercise every control path. A deterministic walker called Evaluate walks the clause chain for any applicant and produces an auditable verdict. If the applicant reached the final clause and was still denied, we have found a temporal deadlock, the shape of "complied with everything and lost anyway."

From there a second Jac Walker, Minimise, runs delta debugging on the counterexample: it deletes one factual precondition at a time from a detached copy of the applicant, re-runs Evaluate after each deletion, and proves which facts are truly load-bearing. This gives us a one minimal counterexample. The proof is in the graph, not in any prompt.

Then the agent loop runs. An LLM receives three tools: list seeded cases, read a clause, evaluate a case. It reasons through them and proposes a typed repair. But it cannot decide anything. Jac validates the draft against every structural constraint, stages two candidates (the narrow proposal and an overbroad strawman), and a third walker called Regress tests both against all seven controls. The target case must flip from denied to eligible while nothing that should stay denied actually does. Only then can the proposal be frozen, sealed with a SHA two five six, and compared against the real government amendment published in the Federal Register four hundred and forty pages away.

What we learned:

Jac graphs are not data structures you model and then reason about. The graph IS the logic. Clause precedence is edge creation order. The counterexample proof is 19 dry traversals that persist nothing to the audit trail. Every claim about determinism is tested by counting Outcome nodes before and after. Forty seven tests cover the evaluator, the minimiser, the regression, the freeze gate, and the blind zone between what the model can see and what it can decide.

We learned that "the LLM proposes" is the easy part. The hard part is making sure Jac decides every downstream fact with no place for the model to slide past its boundaries. The typed byLLM draft becomes a real PatchCandidate node on the graph if it passes validation. A staging receipt records what it looked like on arrival before validation could replace it. The freeze writes once and refuses to rewrite if anything moves. Every dishonesty vector was traced, one at a time, with a test that asserts the engine says no.

How we built it:

Phase one was the policy graph in engine/policy.jac and the evaluator walker in main. jac. We seeded eight hundred and ninety-seven words of regulation text into Clause nodes linked by Precedes edges, created seven applicant profiles from the real case book, and wrote Evaluate to walk head to tail. Forty-seven tests ran before any agent touched the codebase.

Phase two was the control pack, replaying all seven cases with correct historical outcomes, and the live byLLM ReAct loop against a local model. We verified byte-identical reruns twice. The graph persisted in jac persisted between runs, so we had to clean it between test passes.

Phase three added the minimiser walker with delta debugging, the typed draft validation that refuses any proposal targeting the wrong clause, the regression walker that tests broad and narrow candidates against every control, and the append-only freeze with SHA two five six integrity verification. The answer key lives in a separate file that is unreachable until after the freeze, so the model cannot cheat it.

We split across two people: engine on main.jac, policy.jac, clauses.jac, repair.jac, and answer_key.jac; client on frontend.cl.jac, engine_client.cl.jac, and frontend.css. The agent never touches TypeScript.

Challenges we faced:

The ReAct loop against the local thirty-five billion parameter model crashes roughly one in three times inside litellm forced finish. We gave it one retry before falling back to the deterministic detector and saying on screen which path produced the result. One retry converts that to about one in nine because the failure is a non-deterministic sampling artefact, not a property of the request.

Jac client bundling traps two failures that pass jac check but die in the Vite build: graph references inside f strings crash the checker with no line number or file hint, and sem values take adjacent string literals not plus concatenation. A port squatting issue breaks jac start RPCs silently because the dev server serves an unhashed styles.css from a previous session.

The trickiest architectural challenge was ensuring the model's draft is really what gets frozen. We had to make the staging receipt append-only, compare it against the staged PatchCandidate on all five fields, and refuse any freeze where they disagree. The answer key must stay locked until accepted, plus frozen plus verified. Three conditions or nothing.