Back to blog
Claude's 180 Million Lines of Proof: What Formal Verification Actually Proves
“180 million lines of proof” sounds like a declaration that internet software is now free of vulnerabilities. An engineering team needs a more precise question: which executable was proved, what property does the theorem state, which inputs and operating assumptions apply, and what controls are still needed in production? This guide combines Anthropic's formal-verification research with its separate attack-surface reduction research. It is written for security engineers, open-source maintainers, and technical leads who want a reproducible way to read the evidence and choose a small pilot.
The projects address different failure modes. Formal verification aims to establish a machine-checked no-crash property for particular binaries under a defined model. Attack-surface reduction looks for code that an attacker can reach even though the deployment does not need that path. The first is not a certificate that an entire product has no bugs. The second is not a list of hundreds of exploitable CVEs. Confusing them leads to weak procurement decisions and misleading release claims.
Put the headline numbers back inside their claims
Anthropic reports about 180 million lines of Rocq proofs for 239 entry points across 123 open-source libraries drawn from OSS-Fuzz. The proofs concern compiled RISC-V instructions, not every build of the source code on every supported platform. Under the stated model and assumptions, the verified entry points do not crash through memory-safety errors or failed assertions for inputs up to 64 MB. The team says it first patched bugs that obstructed the property and then proved the relevant result for the modified program.
An entry point is not a complete application. A library count is not a percentage of the internet that has been secured. The proof-line total describes the generated proof artifacts, not application code written by a model. Volume is evidence of automation scale and of why a proof checker matters: maintainers cannot reasonably inspect 180 million lines by eye. The meaningful questions are whether the theorem expresses the intended property, whether the trusted model is adequate, whether the executable is the one deployed, and whether verification can be reproduced.
Figure 1. The research illustration shows fuzzing exploring concrete inputs while potentially missing paths; formal proof instead states a property over all inputs within a defined scope.
The separate attack-surface study reports 493 issues across 25 projects. That is a research classification total, not 493 confirmed exploitable vulnerabilities. The findings include unnecessary code reachable before authentication, paths that execute or record state early, and configuration combinations that weaken a configured control. Each case needs its own trigger analysis, severity assessment, maintainer review, and fix status. Do not transform a study total into a vulnerability leaderboard.
Trace the proof from source to checked artifact
The work did not ask a model to announce “I reviewed the code.” It started with existing OSS-Fuzz entry points and compiled the library plus test harness into a RISC-V executable. The researchers combined that executable with formal semantics for RISC-V instructions and Linux processes. From this, they stated a no-crash property. Claude generated the Rocq proof, while the Rocq kernel checked whether that proof satisfied the specified theorem. An invalid derivation is rejected regardless of how plausible its natural-language explanation sounds.
This division of labor is useful. A model can produce a very large amount of routine proof work, while a comparatively small checker decides whether the resulting derivation is valid. Anthropic says it published a subset of the proofs and trusted components so others can independently inspect them. However, a kernel accepting a proof says that the proof follows from its axioms and semantics to the stated theorem. If the theorem omits the behavior the team cares about, if the OS abstraction misses something important, or if production runs a different binary, the checked result cannot be copied into a production guarantee without more work.
Figure 2. The research depicts proof dependencies shared across components; each claim still needs its instruction semantics, theorem, and checker examined.
The published assumptions are material. The program is a single-threaded static binary with a fixed memory budget on RISC-V under a modeled Linux operating system. Inputs are bounded at 64 MB. Thus “all inputs” means all inputs within that bound and within the chosen entry point and environment. Dynamic linking, concurrency, a different architecture, unmodeled system behavior, or larger input requires further modeling and proof. The research presents a path toward broadening scope, not evidence that the current proof already covers those variations.
There is a second operational detail: Claude may patch the program before proving the corrected version. Deployment therefore needs more than a “proof passed” badge. Save the patch diff, review whether it changed intended behavior, run regression tests, and confirm the production build hash matches the proved binary. Otherwise an overly narrow goal could be satisfied by removing a troublesome feature rather than repairing it. The authors describe measures to discourage this kind of reward hacking, but a downstream team must still audit its own acceptance criteria.
No crash is valuable, but it is not “secure”
A no-crash guarantee can be valuable for parsers, decoders, and libraries that process hostile input. Yet a program may exit normally while revealing a secret, accepting an unauthorized request, returning an incorrect answer, or consuming too many resources. A formal proof covers the property that was expressed. It cannot certify properties never written into the theorem. This is why business invariants, authorization rules, confidentiality, side channels, supply-chain integrity, and deployment configuration remain separate work items.
Review a result at three levels. First, the object: which entry point, which source commit, which compiler settings, and which binary hash? Second, the property: exactly what condition is ruled out, and which failure modes remain possible? Third, the environment: do CPU, OS, threads, memory, external services, and input bounds match production? A mismatch in any level should be recorded as uncovered scope. It should not be hidden behind a broad “verified safe” label.
Figure 3. The checker can reject an invalid proof; it cannot judge a business requirement that was never formalized.
The work is also expensive. Anthropic notes that complex proof attempts can consume hundreds of millions of tokens, before accounting for failed runs, patch work, independent review, and ongoing maintenance. A normal business service should not assume it is economical to prove the entire codebase in one pass. A high-risk parsing entry point with a stable harness, explicit input boundary, and clear property is a better first experiment.
The OpenSSH example is about reachability, not a new CVE
In the attack-surface study, Claude traced input paths in OpenSSH 10.4's sshd. The researchers found roughly 4,500 lines of experimental ML-DSA-44 signature code reachable by an unauthenticated client even when the algorithm was not enabled. The relevant checks originally occurred after parsing. Version 10.5 moved a check earlier, but the team then found gaps involving a mismatch between the advertised algorithm and encoded key type, and a certificate CA-signature path. Following work with maintainers, version 10.6 placed allow-list checks before the corresponding parsing or signature verification.
The observation is not that ML-DSA was broken, nor that the reachable code was demonstrably exploitable. It is that complex pre-authentication code need not be exposed when a configuration has not enabled that capability. Reducing reachability can limit the impact of bugs that have not yet been discovered. Anthropic reports that the change removed roughly one fifth of the OpenSSH code previously reachable by an unauthenticated client in a default build. That is a code reachability measure, not a measured one-fifth reduction in breach probability.
Figure 4. Counts indicate where investigators found unnecessary reachability; they do not grade exploitability on their own.
To examine your own service, choose one external-input path into a sensitive parser: an HTTP request before authentication, a plugin loader before permission checks, a deserializer before type validation, or a database protocol handler. Draw the actual call sequence from input to type recognition, authorization, and parsing. Ask: can a disabled feature's parser still run? If it appears possible, confirm with code tracing and a reproducible test. Do not label it a vulnerability solely because the path looks surprising.
A seven-day verification pilot
Day one: select a narrow target with a reason to care. A public image parser's fuzz entry point or a pre-authentication protocol path is better than “prove our entire product secure.” Write down the property and the production risk. Day two: freeze the build inputs, including repository commit, compiler, dependencies, flags, and binary hash. Without that record, later proof results may refer to a different artifact.
Day three: establish a baseline with unit tests, fuzzing, and static analysis. Record known crashes, input coverage, and unresolved defects. These techniques remain complementary. If the test harness is unstable, formal work will be obscured by environmental problems. Day four: list the trusted components: instruction and OS semantics, checker version, theorem statement, and reviewer. Store these alongside the result rather than inside one engineer's chat history.
Day five: run one small task. Either prove one entry point's no-crash property under an explicit bound, or analyze one pre-authentication path for disabled-code reachability. If the model proposes a patch, separate changes needed for the property from unrelated behavior changes and add a regression test for each. Day six: ask another maintainer to review the theorem, the build identity, the patch, and the unmodeled behaviors. Day seven: publish an internal pilot record with four columns: proved, tested but not proved, outside scope, and pending human decision.
| Record | Required evidence | Reason to reject |
|---|---|---|
| Verified artifact | Commit, build flags, binary hash, entry point | Cannot reproduce the same build |
| Theorem | Exact property, input limit, operating assumptions | Only says “secure” |
| Trusted base | Semantics, checker and versions | Critical models have unknown origin |
| Patch | Diff, regression tests, behavior changes | Removes functionality to make proof easy |
| Production fit | CPU, OS, threads and dependencies compared | Copies a RISC-V claim onto another platform |
| Operating cost | Tokens, compute, reviewer time, maintenance | Counts the first model call only |
Teams using Code0 or Claude Code for review can keep the theorem, failing test, patch, and reviewer comment as distinct artifacts. Avoid giving one agent both the author and final approver roles in the same unreviewed session. If models are routed through Apito or another gateway, keep request and billing records while limiting access to source code, vulnerability details, and secrets. A gateway can help with accountability; it does not decide whether a proof is sound. That determination still rests on the checker, the stated theorem, and independent human review of scope.
Where to invest and where simpler controls come first
The strongest first candidates share three traits: external input is reachable, failure consequences are high, and the relevant property can be expressed narrowly. Media parsers, file-format processors, protocol implementations, and critical pre-authentication paths fit this pattern. A service dominated by third-party integrations, dynamic configuration, and manual processes may reduce risk faster through least privilege, input limits, fuzzing, patch management, and rollback drills than through a premature whole-system proof attempt.
The two research methods can be combined. Remove unnecessary paths first, then prove selected properties for the high-risk paths that must remain. That can shrink the proof burden. But a removed path still needs compatibility testing, and a proved path still needs permission and runtime controls. Neither method turns a research statistic into a blanket production warranty.
Before claiming a security improvement externally, answer six questions: can the proof be checked independently; does its theorem cover the risk you claim; has any proposed fix reached the deployed version; does the deployment hash match the verified build; are runtime assumptions still true; and can the cost be sustained as the software changes? An unanswered question belongs in the limitations column, not in a marketing claim.
Preserve verification evidence in a Code0 development workflow
Keep the proved commit and binary hash, theorem statement, checker log, and model-suggested patch as separate traceable artifacts rather than saving only the agent's summary. Ask an independent maintainer to compare the proved version with the version about to ship in every merge review. If build flags change, flag the previous proof for reassessment. The resulting audit trail answers what a specific release guarantees instead of burying environment differences under a generic “passed” status.
Sources
- Anthropic formal-verification research
- Anthropic attack-surface reduction research
- OSS-Fuzz project
- Rocq proof assistant
FAQ
Do 180 million lines of proof mean all 123 libraries are bug-free?
No. The result covers specific entry points, binaries, input bounds, operating assumptions, and a stated no-crash property. Authorization errors, data leaks, logic mistakes, and production differences need separate analysis.
Is human code review unnecessary after Rocq accepts a proof?
No. Rocq checks a derivation against a theorem. People must decide whether the theorem is the desired property, whether the semantics match reality, whether patches preserve behavior, and whether the deployed build is the one proved.
Does the OpenSSH case show that ML-DSA was broken?
No. The reported issue was unnecessary pre-authentication reachability of code when the algorithm was not enabled. The fix moved configuration checks ahead of relevant parsing and verification. This does not establish that the algorithm was compromised or the path was exploitable.
Can a service running on x86 reuse these RISC-V binary proofs?
Not as a direct production guarantee. It needs the appropriate architecture and OS semantics and a proof checked for its own build. The reusable part is the workflow for specifying properties, checking artifacts, and recording boundaries.
What should a small security team do first?
Inventory externally reachable paths and disable unnecessary functionality. Establish a test and fuzzing baseline. Then choose one high-risk, well-bounded entry point for a verification pilot.
