Claude can write the proof. You still have to choose the theorem.

A bounds check can look completely reasonable and still accept a payload larger than its buffer. Here is the offending idea:

payload length + header length <= buffer capacity

It works over ordinary nonnegative integers. It can fail when the addition wraps around before the comparison. The theorem you ask a solver to check has to describe the arithmetic your program actually uses.

That is the part I want to keep in view while reading Anthropic and Theorem’s formal-verification work. The reported result covers 239 entry points across 123 OSS-Fuzz libraries, using Claude-produced proofs checked by Rocq. The guarantees concern specified compiled programs under stated execution assumptions; the authors explicitly distinguish this from removing every possible bug. [1]

I built a small Z3 example to make the specification boundary tangible. It finds a counterexample for a wrapping guard, then establishes the corrected guard’s property in the stated model. This is a standalone arithmetic illustration, not a reproduction of that Claude/Rocq pipeline. 🔎

Computed teaching example: all 256 unsigned 8-bit lengths, an 8-byte header and a 64-byte capacity. The solver example below separately uses unsigned 32-bit lengths.

The bug is hiding inside “plus”

Suppose an unsigned 32-bit length is 4,294,967,288, which is 2**32 - 8. Add an eight-byte header using 32-bit wrapping arithmetic and the result becomes zero. A guard comparing that zero with a capacity of 64 accepts it.

The actual mathematical total is 4,294,967,296. Your allocation did not become that big just because the counter came back around. The arithmetic has performed a very convincing disappearing act. 🪄

For this example, the repair is to compare the length with 64 - 8 before adding. With those fixed constants, accepted lengths cannot exceed 56. If the capacity and header were variable, the implementation would also need to handle the case where the header exceeds the capacity before subtracting.

⚠️ A proof over unbounded integers would miss the original issue if it silently replaced wrapping addition with ordinary addition. The math could be correct while modeling the wrong operation.

Z3’s bit-vectors let me state the finite-width arithmetic explicitly. Its unsigned comparison operations are ULE and UGT; the ordinary comparison syntax on bit-vectors has signed meanings. That choice belongs in the specification too. [2, 3]

Ask for the violating input

Save this as guard_demo.py and run:

uv run --python 3.12 --with z3-solver==4.15.4.0 python guard_demo.py

from z3 import BitVec, Solver, ULE, UGT, ZeroExt, sat, unsat

length = BitVec("length", 32)
bad = ULE(length + 8, 64)
actual_total = ZeroExt(1, length) + 8
s = Solver()
s.add(bad, UGT(actual_total, 64))
assert s.check() == sat
print("wrapping guard admits an oversized payload:", s.check())

fixed = ULE(length, 64 - 8)
s = Solver()
s.add(fixed, UGT(actual_total, 64))
assert s.check() == unsat
print("corrected guard admits an oversized payload:", s.check())

n = 2**32 - 8
assert ((n + 8) % 2**32) <= 64 and n + 8 > 64
print("witness:", n, "+ 8 =", n + 8, "but wraps to", (n + 8) % 2**32)

false_accepts = [n for n in range(256)
                 if ((n + 8) % 256) <= 64 and n + 8 > 64]
assert false_accepts == list(range(248, 256))
assert all((n <= 56) == (n + 8 <= 64) for n in range(256))
print("8-bit exhaustive false accepts:", len(false_accepts))

My output:

wrapping guard admits an oversized payload: sat
corrected guard admits an oversized payload: unsat
witness: 4294967288 + 8 = 4294967296 but wraps to 0
8-bit exhaustive false accepts: 8

sat means the solver found an assignment satisfying the constraints. Here, those constraints say that the guard accepts the payload and the actual total exceeds capacity. Finding a satisfying assignment exposes a bad acceptance.

For the corrected guard I ask the same question. unsat means there is no such assignment in this model. That is stronger than checking a handful of lengths, because the symbolic question includes every unsigned 32-bit length. ✅

The ZeroExt operation deserves a look. It widens the length to 33 bits before adding the header. The widest possible 32-bit length plus eight fits in that larger representation. I use that expression to describe the actual total without repeating the overflow inside the property I’m trying to check.

The short Python enumeration is an independent check of the smaller 8-bit picture. It visits every length from zero through 255 and confirms that the bad acceptances are exactly 248 through 255. The corrected condition agrees with the ordinary-integer capacity test throughout that smaller domain.

A checked proof still has a boundary

The research pipeline operates on compiled RISC-V binaries with formal execution semantics and a proof checker. Its trusted pieces include the theorem statements, the execution models and the checker itself. Its stated assumptions include single-threaded static binaries, a fixed memory budget and a bounded input size. Those details determine what the result covers. [1]

My tiny example has its own boundary. It models a length guard, not a parser, an allocator, a compiler or a complete program. It does not prove that a real buffer has the declared capacity. It does not establish that every caller uses this guard, or that another operation later corrupts the length. Z3 checking the logical query is also a different verification path from replaying a Rocq proof.

💡 The practical review question is: what would a bug outside this statement look like? For the guard, it could be an incorrect capacity, a signed conversion before the check, or a different arithmetic width in the implementation. Writing those possibilities down tells you which assumptions need evidence and which properties need another statement.

AI can help produce a proof artifact at a scale that used to be hard to contemplate. The developer still needs to recognize whether the checked statement answers the question that made the code risky in the first place.

References

1. Anthropic and Theorem: formal software verification at larger scale.
2. Z3Py guide: machine arithmetic and unsigned bit-vector operations.
3. Z3 Python API reference.

Asset credit: original chart from exhaustive enumeration of the synthetic 8-bit guard.

AI disclosure

AI was used to draft the article.