Both AI reviewers caught the same bug. If a camera answers a position query with blank values, the code I was testing reads blank as zero. It moves the camera, then "restores" it to pan zero, tilt zero, zoom zero, and signs a record saying the restore was verified. The camera is now pointed wherever zero is, zoomed all the way out, nowhere near where it started. The record says verified.

I found that while settling a bet about proof tools.

On September 22, Boris Cherny at Anthropic posted that he had used Claude "to formally verify the Claude Agent SDK using Lean," a proof assistant, and added that "TLA+ also works well." By the next day he had narrowed it himself. "'Verify' is a little loose yeah," he told one reader, and he explained to the formal-methods people that the hairiest parts of the code were being modeled and checked for counterexamples, not the whole thing proved. Fair. The work looked real, and three AI models I had read the thread said the same. But the experiment nobody had run was still the plain one. Same code, same day, one pass with a proof tool and one without. Count the bugs.

For my last years on the job I was the sergeant reading other people's reports. The template never caught what I caught, because the template only asked the questions its author thought to ask. A proof is the strictest template there is. It checks exactly what it was told to check, about a model of the thing. The second reader checks the thing. So the bet was really this: does a proof tool find what a second reader doesn't?

I wrote the prediction down that night, let it slip five weeks, and on October 30 ran it twice.

The first test used a tool I maintain for talking to my own cameras. One loop, about 650 lines: plan a change, apply it, read the camera back, roll back if it doesn't match. The formal pass wrote a TLA+ specification of that loop, ran the TLA+ model checker over every sequence of lost replies, rejected writes, crashes and a second writer it could explore, then replayed 43 real runs from my cameras' receipt log through the model. The control was the same AI model in a fresh window with the same code, allowed to read the tests and run probes, and one prompt: find races, stuck states, and double-guard bugs. No spec. My rule: a finding counted only if a test failed on the untouched code and passed on a small fix.

The formal pass found seven bugs. The review found all seven, plus nine more. The formal pass's one unique find was a real violation of a rule I'd written down, with no clean fix. By the rule I wrote in September it would have held, by one. I'd added the fix requirement the day before the run, and that's what dropped it. Under the rule I registered, the prediction failed.

The formal pass wasn't worthless. It showed that a handful of properties held under every sequence it explored, which a reviewer can never say. And its replay found five signed handoff files already in the repository claiming a rollback that never happened. Review found the same bug. Only the replay found the files it had already touched.

Then I changed the reader instead of the method. I gave the same code to a model from a different company, OpenAI's Codex, with the requirements and the spec, and none of the findings. Codex had worked on this code before, in overnight build runs, which makes what came back more interesting, not less: seven more bugs neither pass had seen, and one I'd thrown out that it argued back in. Twenty-four, on one commit of a tool I'd used for months.

The second test was designed to Codex's rules. It had said my fix requirement punished the structural bugs a proof tool is good at, and that "the prover is overhead" was more than my data showed. It wrote the rule it would accept: reproduce the failure on the untouched code, judged by someone who built neither arm, no fix required. I registered that rule and its prediction before anything ran, and picked code neither model had seen in this study: the part of my open-source evidence project that moves a camera to a preset, polls it, restores it, and survives a crash halfway through. About 700 lines. Codex had built it, in July.

This time the reader stayed the same and the method changed. Two fresh copies of one model, same brief except for the method, two hours each. The formal arm finished in 18 minutes, the review arm in ten and a half. Codex judged every candidate on the untouched code and ran each probe twice.

Ten bugs. Six found both ways. One by review alone, because the model's clock was a tick counter and the code's clock was the wall. Three by the formal arm alone. Two of those it noticed while writing the spec, not from the checker, and one of the two is serious: a stalled credential lookup leaves the camera off its position with no restore. The one the checker itself produced was real and reproduced, and it can only happen through a test transport. The shipped network path can't trigger it. Low severity.

The prediction held, by one, and that's how narrow the one is.

The blank-to-zero bug came from both arms. Either reader alone would have caught it. Here is the stake. After an operator pans a camera, the restore is what puts it back on its post. With this bug the camera watches the wrong scene for as long as nobody looks, and a signed record says it's back. That's the footage a detective goes looking for, and the record a defense attorney reads aloud.

What one day and two runs taught me, as judgment and not as a ranking: changing who read the code moved the count more than changing how. A second pass found nine. A blind reader from another company found seven. The checker found none under my rule, then one under its own. Writing the spec made its author a careful reader, and two of the formal arm's three unique finds came from the writing. The checker itself gave me guarantees about what it explored and one narrow catch, at half again the time.

If you're buying a system that keeps records a court will see, ask the vendor who outside the build team reads the code, and whether you can see what they found.

Who ran all of it? Me, every time, with Claude Code writing the specifications, the probes and the tests on my own machine, and Codex reading blind.

My day job is selling AI to police, and before that I worked for Axis, whose cameras both of these tools drive. Both tools are open-source projects I maintain, worked on my own time. The first test replayed receipts from my own cameras on my own network. The second touched no camera at all.

For the people who run an evidence or records system: when did your vendor last show you what a second reader found?

The record said verified. Nobody had asked what the code did with a blank.

Lab: Test 1 on onvif-mcp commit fa37745, test 2 on aar commit ae909f7, both October 30, 2026. TLA+ with TLC 2.19. Claude wrote both specifications and ran both review passes in fresh windows (Claude Opus 5.5 for both arms of test 2). OpenAI Codex (GPT-6 Astra) ran the blind pass on test 1 and judged test 2. Requirements, predictions, spec files, model-checker traces, probes and both judges' write-ups are in my working notes. Built and checked with Claude Code.