Nothing this week could prove itself
Checking is being packaged and sold in the same week that the artifacts meant to prove correctness, formal proofs and model reasoning traces alike, turn out to persuade nobody on their own
What makes anyone believe a program is correct was the week's live question, and none of the answers was a proof. A rereading of the classic case against formal verification argues that proofs get accepted through social processes: people read them, argue about them, build on them, and eventually stop objecting. Nobody is ever argued into it by the symbols alone. The newest candidate for a trustworthy artifact, the scratch work a model writes out before answering, is meanwhile coming apart under attack. We argued a while back that review capacity, not model capability, was the constraint, and the commercial follow-on is now visible: checking is being packaged and sold, starting with a code review platform from a coding-tool vendor. Which leaves exactly the gap the verification people identified half a century ago. Somebody still has to do the social work of believing the artifact. The tell will be what these products emit: evidence a reviewer can check, or just a verdict.
Top Stories
The case against formal verification still holds 50 years later. Ivan Gavran revisits the social-processes argument, which held that a proof about a program gets believed the same way a mathematical proof does: people read it, poke at it, build on it, and eventually stop finding holes. Writing it down formally does not do that part for anyone. That lands differently now that proofs and programs are both cheap to produce, because the pile of unread artifacts grows on both sides at once. A proof nobody has read sits in roughly the position of a test suite nobody wrote: it is evidence exactly to the degree that somebody has done the work of trusting it, which is to say none.
A model's reasoning trace is not a safe place to keep anything. A reasoning trace is the thinking a model writes out before its answer, the part providers usually hide and treat as sealed. The work gathered as Stolen Thoughts goes after exactly that, and the recent results all point one direction. Thinking tokens can be steered by ordinary-looking text sitting on a page the model happens to read. Content can be pulled back out of reasoning blocks the provider considers private, with a weaker jailbroken model doing the reading. So two properties break at once: the scratch work stops being private, and it stops being reliable evidence of what the model actually did. Anything downstream that reads a trace to judge whether an action was reasonable inherits both problems, and this line of attack looks early rather than finished.
A coding-tool vendor is turning review into a platform. Cursor is preparing to launch Origin, a platform for code review. The sequence is not subtle: generation got cheap, the backlog moved downstream to reading, and now the tool that created the backlog sells the cure. But the shape is the more interesting part. Owning generation and owning the check on generation is the same vertical bundle every large platform is assembling this year: data plugged into agent plugged into the thing that grades the agent. Bundles like that usually price well and reason poorly about their own output.
From Antfly
Antfly v0.2.0 shipped, pulling separate components into one repository and one release:
- the proxy, the Kubernetes operator and the Termite ML service now live in the monorepo, with the ML API served under /ml/v1/
- AFB, a portable backup format that moves a backup across storage backends
- a serverless operator and proxy, with TLA+ trace validation running in CI
Top Links
- rd-signal-2: Frontier Classification at Production Scale (raindrop.ai): classification at production volume, where the economics have rarely favored the largest model on offer.
- DeFlock (deflock.org): a project pointed at the private license-plate reader networks that some cities have begun backing out of.