Anthropic reports AI-written proofs for selected software tests

What the researchers reported

On October 22, Anthropic and Theorem described using Claude to produce machine-checked proofs for 239 test entry points across 123 open-source libraries. Some code was patched before being proved. The results concern specified properties of compiled binaries, not every behavior of those libraries.

The setup assumes single-threaded, static RISC-V binaries on Linux, a fixed memory budget and inputs under 64 MiB. Guarantees depend on the modeled machine, operating system, theorem statements and proof checker. They do not establish that deployed software is free of all bugs. The report provides no measured employment effect or controlled comparison of human labor time.

Sources: Anthropic — LLMs are making formal software verification feasible at a much larger scale; Anthropic — Formal verification research appendix

Our interpretation: make the boundary readable

For developers and security analysts, we see a useful learning exercise here: explain a technical guarantee to the person deciding whether to ship a change. A passing check becomes more useful when that person can understand which question it answers. This is our suggested practice, not a finding about changing hiring requirements.

Imagine a team evaluating a parser used to read uploaded files. One engineer prepares a short note naming the exact build being assessed, the permitted inputs and the behavior the check covers. A colleague then compares that note with the production service. Does the service use the same build? Can an upload exceed the stated limit? What happens before the parser receives the file?

The exercise can finish with two columns: evidence we have and questions still open. Assign an owner to each open question before deciding what additional review is appropriate. A mismatch need not make the evidence worthless; it tells the team where its argument needs more work.

For someone building a portfolio, a concise explanation of those decisions could be more informative than a screenshot showing a successful check. Include one hypothetical change that would require reassessment, and explain why. We suggest this as a way to demonstrate technical judgment; we are not claiming employers have adopted it as a hiring test.