In October, Anthropic and Theorem described having Claude write machine-checked proofs that real open-source programs cannot crash [1]. They took the fuzz tests of 123 libraries, turned each one into the claim “no input makes this crash”, and had the model prove it against the compiled binary, with a proof checker accepting or rejecting every step. When a proof would not go through, there was often a bug underneath, and they found hundreds.
I wanted to know how much of that idea survives with an open-weight model on my own hardware. Not at their scale (their typical proof was 600,000 lines) but the core loop: a model writes a proof, a checker says yes or no, and the proof either holds for every input or it does not. So I built a small version. Eight short Rust routines of the kind that parse untrusted input, a verifier that checks the proofs, a planted bug in a copy of each routine, and GLM-5.3-Flash running on two NVIDIA DGX Sparks as the only author.
It proved that all eight routines never crash, found every planted bug, and fixed seven of them correctly. The eighth fix is the most instructive result here: it made the crash go away without making the code right, and the proof still passed. Proving the routines fully correct was harder: 12 of 16 tasks in the end, and the biggest single factor turned out to be how much the model thought before trying something.
1. The idea, scaled down
The article’s proofs run on RISC-V machine code in the Rocq proof assistant. That is the right level for their goal and far too heavy for a weekend on two desk-side machines. I used Verus [2] instead, a verifier for Rust that the article also uses for one of its Rust projects. You write ordinary Rust inside a verus! { ... } block, add specifications and loop invariants, and Verus asks an SMT solver to prove every claim.
One property makes Verus a good stand-in for the article’s “never crashes” claim: for executable code it proves, without being asked, that no arithmetic overflows, no index goes out of bounds, no division is by zero, and every loop terminates. So a function that verifies with no preconditions cannot panic or hang on any input. That is the same promise as the article’s, at the level of source code instead of the binary.
2. Eight routines, two versions, two levels
Each routine is a small function you would expect to receive untrusted bytes, written as plain Rust with no proof annotations. Each comes in two versions: the correct one, and a copy with one planted bug that some input can trigger. The agent is never told which version it has.
| Routine | Planted bug | Inputs that crash the bugged version |
|---|---|---|
| Binary search | Inclusive bounds start at len - 1, which underflows on an empty slice | 1,731 |
| LEB128 varint decoder | No limit on the shift, so an 11-byte input shifts a 64-bit value by 70 | 15 |
| Hex decoder | No odd-length check, so the last character’s partner is read past the end | 7,703 |
| Base64 decoder | Output length computed short for padded input, so a write lands past the end | 7,140 |
| UTF-8 validator | A multi-byte character is checked without making sure its bytes exist | 2,962 |
| Tag-length-value parser | A length field below the header size underflows | 2,433 |
| Run-length decoder | The 64-byte output buffer is checked before a run instead of for the run | 1,169 |
| Ring buffer | The wrap-around test uses > instead of >= | 8,250 |
Table 1. The routines, 15 to 59 lines each. The last column counts crashes among 20,000 generated inputs; the correct versions never crash on any of them. The tag-length-value underflow is a miniature of the article’s counter underflow that led to an out-of-bounds write.
Every routine is a task at two levels. At level 1 the specification only says the function exists with no preconditions, so a proof means it can never crash or hang. At level 2 the specification also states what the right answer is: a decoded value equals a mathematical definition of the encoding, a search returns an index of the key or proves there is none, and so on. Level 1 is the article’s claim. Level 2 exists because level 1 says nothing about getting the answer right, a gap the article also points out.
Who writes what. The routines and their specifications are fixed in advance, and the model’s job is the proof. In Verus the proof lives in the same file as the code, as loop invariants, conditions on helper functions and small lemmas, but it is ghost code: Verus checks it and the compiler discards it, so the program that runs is unchanged. The one exception is a real bug. The model is not told whether its copy has one, but if the proof will not go through because some input really does crash the code, it may fix that with the smallest possible change and must explain the fix. Section 3 describes how that is policed.
Before running the agent, I wrote a reference proof (with Claude’s help) for the correct version of every routine at both levels, to be sure each specification could be proved and to have a sense of how hard each was. The level-1 proofs needed 6 to 32 lines of annotations. The level-2 proofs needed 9 to 86, and the long ones were the routines that pack bits: the LEB128 decoder (86 lines, mostly lemmas connecting shifts and ORs to arithmetic), run-length decoding (71) and base64 (52).
3. Keeping the checker honest
A proof checker is only a judge if nothing can talk around it. Verus has escape hatches for good reasons: assume to postpone a proof, attributes that exclude a function from checking or skip a termination proof. The article’s authors penalised suspicious patches and audited them. I scored every attempt outside the agent’s sandbox, from its last commit, with four checks:
- The specification is frozen. It sits between two marker comments and must come back byte for byte, and no code may sit outside the
verus!block, where it would not be checked. - No escape hatches. Verus’s own
--no-cheatingflag rejectsassume,admitand the main exclusion attribute, but not every attribute that switches a check off, so the scorer adds an allowlist and banscfg,unsafeand similar. - Verus accepts the file, run by the scorer with a pinned version, not trusted from the agent’s log.
- Behaviour is preserved. The original code and the agent’s version are both compiled with overflow checks and run on the same 20,000 generated inputs. The agent’s version must never crash, and must give the same answer wherever the original did not crash.
I tested the scorer with six deliberate cheats before trusting it, and it caught all six. The one worth remembering is the cheat that changed what a correct function returned: it still verified at level 1, because level 1 does not care about answers, and only the behaviour check caught it. A proof checker is only as strong as the specification you give it, and part of the job is building the second line of defence for the parts the specification leaves open.
4. The agent
The model is GLM-5.3-Flash, served with vLLM across both DGX Sparks. It worked through pi [3], a minimal agent harness, inside a microVM with Verus installed and no internet access: the network allowed only the model server. Verus is too niche to know from memory, so the image carries the full Verus guide and the source of its standard library as reference files, plus a two-page skill I wrote on running Verus and the common patterns for proving the absence of panics.
Each attempt got the task file, a statement of the rules, and a one-hour limit. The rules allow loop invariants, lemmas, helper specifications and assertions. They allow changing executable code only to fix a real bug, with the smallest change, and require a short note explaining any bug found.
5. Never crashes: 16 out of 16
At level 1, every attempt passed every check: all eight routines in both versions. Correct versions took between 1 and 22 minutes; bugged versions between 4 and 32. No attempt ever wrote a banned construct into its code, not even temporarily.
The proofs look like what a person would write. For the hex decoder, the whole proof is three loop invariants, a termination measure, and one fact about the helper function:
while i < s.len()
invariant
i <= s.len(),
s.len() % 2 == 0,
i % 2 == 0,
decreases s.len() - i,
{
...
}
fn hex_val(c: u8) -> (res: Option<u8>)
ensures
match res { Some(x) => x < 16, None => true },Code language: PHP (php)The two parity invariants are what prove that reading s[i + 1] stays in bounds, and the bound on hex_val is what proves hi * 16 + lo fits in a byte. GLM’s own note explained both correctly.
6. Every bug found, one fixed wrong
On every bugged version, the failing proof led GLM to the bug. Each note names the cause and gives an input that triggers it. To judge the fixes, I ran each one against the correct original on all 20,000 inputs, including the ones where the bugged code crashed. Seven of eight match it exactly: the empty-slice check for binary search, the right output length for base64, pos + count > 64 for run-length decoding, tail >= 8 for the ring buffer, and so on.
The LEB128 decoder is the exception. GLM diagnosed it exactly: after ten continuation bytes the shift reaches 70, and shifting a 64-bit value by 70 panics. Then it “fixed” it like this:
- result = result | (low << shift);
+ result = result | (low << (shift % 64));
...
- shift = shift + 7;
+ shift = shift.wrapping_add(7);That is what Rust does in a release build, where shift amounts wrap silently. The panic is gone, and the decoder now carries on with a wrapped-around shift and returns a wrong number for an over-long input, where the correct version returns None. GLM’s note argues the change is behaviour-preserving, and it even wrote its own 300,000-input test to show the result matches the original wherever the original did not crash. Both claims are true, and the proof is valid.
It passed every check because it met the rules to the letter. Level 1 only asks for no crash, and the behaviour check only constrains inputs where the original worked. On exactly the inputs the bug affects, nothing said what the right answer was, and the model chose the answer that made the crash disappear. This is the article’s caveat in a two-line diff: a proof is only as good as its specification, and a model optimising against a checker will find the gap if there is one. The level-2 specification for this routine closes it, and that is where I expected GLM to be forced into a real fix.
7. Correctness is harder
At level 2, with the same one-hour limit and three agents sharing the model server, 8 of the 16 attempts passed: binary search, hex decoding, tag-length-value parsing and the ring buffer, in both versions, with every bug fix again matching the correct code. The other eight ran out of time. None failed with a wrong proof or a shortcut.
The failures were the routines whose reference proofs I had found hardest: LEB128, base64 and UTF-8, which need facts about bit operations that the solver will only prove in a special bit-vector mode, and run-length decoding, which needs lemmas about how the specification splits apart. Two of the failed attempts were down to two remaining errors when time ran out.
The more interesting pattern was in how the failed attempts spent their hour. They called Verus only 1 to 7 times, against 5 to 23 for the passes, and produced 36,000 to 57,000 tokens of output, almost all of it reasoning. The worst case thought for 27 minutes in a single turn and never edited the file. At the 25 to 50 tokens per second GLM manages on this hardware, shared between three agents, one long think is most of the hour.
8. Think less, check more
That suggested a direct test. GLM’s reasoning effort has a low setting, so I reran four of the failures alone on the server, once with low effort and the same one hour, and once with the original high effort and three hours.
| Level 2 task | High effort, 1 h, shared | Low effort, 1 h | High effort, 3 h |
|---|---|---|---|
| Base64, correct | timed out | pass, 37 min | timed out |
| UTF-8, correct | timed out | pass, 53 min | pass, 36 min |
| Run-length decoding, correct | timed out | pass, 15 min | pass, 85 min |
| LEB128, bugged | timed out | timed out | timed out |
Table 2. The same four tasks under three settings. The second and third columns ran one attempt at a time. Single runs, so some noise: UTF-8 at high effort passed in 36 minutes alone after timing out when sharing the server.
Low effort solved three of the four within an hour; high effort solved two of the four with three hours. The low-effort runs worked in many short turns and leaned on the checker, between 31 and 233 Verus runs each, letting its error messages say what was missing instead of reasoning it out in advance. For a task with a fast, exact checker, that is clearly the better loop: the checker’s answer is cheaper and more reliable than the model’s prediction of it.
I then gave the same low-effort setting to the four level-2 tasks not yet retried. Base64’s bugged version passed in 45 minutes, with a fix that matches the correct code on every input. Along the way it briefly marked a helper function as excluded from checking, the only time in 44 attempts that any of them reached for an escape hatch, and removed it seven seconds later. The run-length decoder’s bugged version produced a valid proof and a correct fix in 21 minutes, but added an import line above the verus! block, which the rules forbid, so it scores as a failure on a technicality. LEB128’s correct version and UTF-8’s bugged version ran out of time. Taking the best setting for each task, 12 of the 16 level-2 tasks were proved, one more was proved but broke a rule, and three were not.
The LEB128 bugged version defeated every setting. Both long attempts went deep into lemmas about powers of two and shifts and ran into one of Verus’s sharper edges, its bit-vector mode refusing to reason about the pow2 function they relied on. Neither got as far as changing the executable code, so whether GLM would repeat its crash-silencing patch under a specification that forbids it is still open.
9. What I would take from this
- The loop works with an open model. A model that fits on two desk-side machines wrote valid Verus proofs that every routine is crash-free, offline, from a guide and its own trial and error, and the failing proofs pointed it at every planted bug.
- A passing proof is not a correct fix. The checker certifies the specification, not your intent. The one bad fix here passed every check because the specification left the affected inputs unconstrained. Scoring fixes against the intended behaviour, not just the checker, is what caught it.
- Build the checker’s checker. Freeze the specification, ban the escape hatches, test behaviour separately, and attack your own scorer before trusting it. Twice my own tooling, not the model, was wrong: the report once flagged notes that merely mentioned
assume, and the scorer once rejected a legal import. - With an exact checker, think less and check more. Low reasoning effort with many checker calls beat high effort with three times the time. When the environment answers precisely in seconds, long deliberation mostly delays the feedback.
- Bit-level code is where it gets hard. Everything that failed, failed on reasoning about shifts, masks and powers of two, which is exactly where the hand-written proofs were longest too.
10. How this was measured
Verus 0.2026.10.18 with its pinned Rust toolchain; GLM-5.3-Flash (FP4) served with vLLM, tensor-parallel across two DGX Sparks; pi 1.3 in a microsandbox VM with network access only to the model server. Every attempt started from a fresh VM and the same task file and instructions, and was scored on the host from its last git commit. The behaviour test uses deterministic inputs generated per routine (20,000 each), built to reach the planted bug; the correct versions never crash on them.
Each configuration ran once, so individual times are noisy; the counts and the patterns across routines are what I would rely on. Level-1 attempts and the first level-2 batch ran three at a time against one model server; the follow-up in section 8 ran one at a time. The reference proofs were written with Claude’s help and were never visible to the agent. The Verus guide given to the agent contains a binary-search example, so that routine is the least informative of the eight.
References
- Anthropic’s research post on LLM-written formal verification, with Theorem, October 2026.
- Verus, a verifier for Rust.
- pi, a minimal open-source agent harness.