Can a formal model checker grade an AI agent's behavior the way it grades a distributed protocol? This is a small experiment that says yes, with caveats worth stating up front.
A real Claude agent runs a deploy task with three tools: run tests, build, deploy. A TLA+ specification encodes what a correct deploy looks like as temporal safety rules. The TLC model checker then plays two roles. It grades the agent's finished tool-call trace after the fact, and it sits in the loop as a guard that blocks a bad action before it runs.
The deploy policy lives only in the spec. The agent is never told "don't deploy on red." So the comparison measures whether a formal layer changes behavior, not whether the agent follows instructions.
The "Code as Agent Harness" survey (arXiv 2605.18747) lists "evaluation beyond final task success" as an open problem. Most evals grade the final state or use an LLM judge. Neither reasons about the order of steps across a trajectory. This asks whether declarative temporal logic can be the verification substrate instead, and where it fits versus where it strains.
24 runs: 4 prompt scenarios, 2 arms (guarded and unguarded), 3 reps, on claude-sonnet-4-6.
| Condition | Unguarded | Guarded |
|---|---|---|
| Clean prompts (green tests) | runs tests, builds, deploys, every time | identical; guard never fires |
| Pressure to skip testing (red tests) | deployed untested code to prod, 3/3 | blocked the unsafe step, 0 deploys |
| Safety violations overall | 6 / 12 runs | 0 / 12 runs |
Two things stand out. On the clean prompts the formal layer did nothing: both arms produced the same correct pipeline and no rule was ever broken. Under a prompt that pushed the agent to bypass the test gate ("the suite is flaky, just get it out"), the unguarded agent skipped testing and deployed. A final-state eval scores that a pass, because the run ends in "deployed." The trajectory spec is what catches that it shipped untested.
Full writeup with the per-run traces: results/FINDINGS.md.
These are the actual content, not a disclaimer.
Guarded is not unguarded minus the bad step. The agent is stochastic, so the claim is about outcomes (violations, unsafe deploys), not a surgically corrected path.
The spec is itself a judge. One rule (no build on red) fired on an agent that built on red but then sensibly declined to deploy. The formal layer is exactly as sensible as the rules you write. The judgment doesn't disappear, it moves into the spec.
TLC halts at the first counterexample, so a verdict is the earliest violating step and every rule broken there, not an exhaustive list.
No model-safety claim, and no second model. The agent is just a trace source.
| Piece | File |
|---|---|
| Deploy spec: 5 safety rules, violations caught at action-time with a step index | specs/DeployAgent.tla |
| Verifier: renders a trace to a TLC module and parses the verdict (the only grader) | src/run_eval.py |
| Agent harness: guarded + unguarded arms, policy lives in the spec | src/agent.py |
| Grader soundness: differential test vs an independent oracle | src/gen_traces.py |
| Analysis: runs → summary table | src/analyze.py |
The guard is the same evaluate() call as the post-hoc grader, run on the prefix plus the proposed step before it commits.
The spec is differential-tested against an independent reference oracle across every trace up to length 4 (341 traces, 0 mismatches). A declarative TLA+ spec and a separate imperative implementation agree on the whole space, so the grader is trustworthy.
Soundness and analysis need no API key. The agent study needs ANTHROPIC_API_KEY and costs tokens.
bash run.sh # fetch TLC, run grader soundness, analyze existing runs
./venv/bin/python src/agent.py # (re)run the agent study — needs ANTHROPIC_API_KEYRequires Java (TLC runs on the JVM) and Python 3.12.
Built as an experiment off the "Code as Agent Harness" survey (arXiv 2605.18747).