---
title: "Claude Generated Checked Proofs for Software. Read the Guarantee Carefully."
description: "Anthropic and Theorem report no-crash proofs for selected library entry points. The precise theorem matters more than the headline."
date: "2026-10-23"
tags: ["developer-tools", "agents", "security"]
canonical: "https://news.maestromojo.com/news/claude-formal-verification-narrow-guarantees/"
---

**Maestro’s take.** Ask the model for a proof that a separate checker can validate. Then scrutinize what the proof promises. A checked answer to a narrow question is valuable.

## TL;DR

[Anthropic and Theorem reported on October 22](https://www.anthropic.com/research/formal-verification) that Claude produced no-crash proofs for 239 entry points across 123 OSS-Fuzz libraries. Claude wrote proofs in Rocq. Rocq’s kernel checked them against Theorem’s formal model of the execution environment.

Claude sometimes patched bugs before proving the resulting binaries. Those proofs do not certify the original versions.

This does not mean 123 entire libraries are bug-free. The work targets particular compiled, statically linked, single-threaded RISC-V Linux programs with bounded memory and inputs under 64 MB. A guarantee for that model does not automatically cover another processor, build or caller.

## Why Maestro users care

A model saying code looks correct is different from a checker accepting a proof. The latter can give builders a precise guarantee—if the theorem, checker and environment model are sound.

Anthropic also describes proofs that consumed hundreds of millions of tokens. This is evidence of a workflow becoming possible, not evidence that full verification is now cheap.

Maestro’s inference: start where one narrow guarantee would justify the effort. A parser that must not crash within explicit input bounds is a clearer target than “verify the application.”

## One thing to try

Choose one fuzz-test entry point. Write down the property, input limits and exact build it should cover. Review the released work linked in Anthropic’s announcement before attempting a pilot. Keep tests for behavior outside that guarantee.

*Published October 23, 2026 · Brief and Maestro commentary · Tags: developer tools, agents, security*

**Original source:** [Anthropic and Theorem’s methods, limitations and released proof links](https://www.anthropic.com/research/formal-verification).