Formal verification with LLMs, in 30 days

What happened: a credible milestone

According to Anthropic, frontier models can now autonomously produce correctness proofs for real-world software at scale. In collaboration with Theorem, they proved security properties at the assembly level (RISC-V) across 123 open‑source libraries. The specific property class they tackled was practical and security-relevant: for certain executable artefacts, the programmes will always exit normally without triggering memory-safety errors or failing assertions, for every input under 64 MB and every modelled Linux OS response and memory layout—under assumptions that the binary is single‑threaded, static, and has a fixed memory budget on RISC‑V with Linux (Anthropic).

While writing these proofs, the model also found bugs that had evaded detection for years despite trillions of test runs—a striking reminder that fuzzing and tests cannot cover all paths (Anthropic). A subset of proofs and the RISC‑V and OS semantics have been published for reuse, and Theorem is offering to run the pipeline for other open‑source projects alongside a Claude skill to help developers get started (Anthropic).

The researchers also discuss the broader challenge: formal verification demands precise specifications and has historically been prohibitively expensive. They outline how LLMs reduce that cost and even describe work on “turning tests into proofs” and exploratory efforts beyond the main pipeline, such as assessing the security of the zlib compression algorithm, proving behavioural equivalence of a Python interpreter written in Rust, and surfacing long‑standing bugs in critical software (Anthropic).

Why it matters for software assurance

Even mature, heavily tested systems still harbour defects, and more capable models can chain smaller flaws into critical exploits; we need guarantees, not just good intentions (Anthropic). Formal methods bring those guarantees when you can state properties precisely and check them exhaustively against a machine‑readable model. The novelty here is scale and feasibility: Anthropic provides evidence that LLMs can draft and iterate proofs for production code, surfacing real issues and proving non‑trivial safety properties at the assembly level under clear assumptions.

This doesn’t eliminate the human role; it changes it. Think of the model as a junior proof engineer: fast at drafting invariants, exploring cases, and porting patterns; you review, prune, and set the bar for acceptable assumptions. Over time, more of the effort shifts from hand‑crafting lemmas to curating reusable proof components and specifications. That’s a materially better posture for software assurance than hoping test coverage is representative.

If you already have static analysis, type disciplines, and runtime checks, now is the time to add targeted formal guarantees. And yes, the traditional ecosystem—proof assistants and model checking—still matters. LLMs don’t replace those techniques; they make them more approachable by automating the labour of constructing proofs and exposing counterexamples early. The result is a better blend of depth (proof) and breadth (tests and fuzzing).

Finally, specifications are still hard. The Anthropic write‑up explicitly highlights that challenge and discusses turning existing tests into a pathway for proofs. Take that as permission to start with property fragments you can state crisply.

Where to start: scope, properties, and the architecture

Begin with a narrow slice of your most critical services—parsers, crypto‑adjacent routines, payment or identity flows, or memory‑unsafe boundaries. The key is property selection: adopt the same style of properties validated by Anthropic—“no memory‑safety errors or assertion failures, exits normally”—under explicit environment assumptions (inputs up to X, single‑threaded, fixed memory budget, OS interactions modelled). Clarity beats ambition at this stage.

Set the collaboration model: the LLM proposes, you dispose. Treat it as a junior proof engineer drafting invariants, proposing lemmas, and refactoring proofs for reuse. You curate a small library of specification patterns for your codebase: parse‑don’t‑panic; bounds‑checked loops; total decoders; safe state transitions; allocation discipline. Over time this becomes your internal proof toolkit.

Architecturally, add a verification lane alongside build/test: a job that consumes build artefacts, the spec fragments, and the proof scripts. The output is machine‑checkable artefacts and a provenance record you can diff code‑to‑proof over time. Keep this lane optional initially, but visible, with results published next to test/fuzz dashboards.

For how to decide between refactoring, modernising and replacing, see modernise or replace.

If you already use proof assistants or model checking, keep them in play. The LLM can help bridge the gap: extracting candidate invariants from code and tests, proposing refactorings to make functions more amenable to proofs, and generating boilerplate proof obligations.

30-day rollout: formal verification with LLMs in CI

Days 1–7: choose scope and properties

– Pick one service or library on your critical path and identify 2–3 high‑value safety properties you can state precisely (e.g., no memory safety violations; no failed assertions; guaranteed normal exit under bounded inputs and modelled OS outcomes).

– Write down environment assumptions explicitly (input bounds, single‑threading, memory budget, OS interactions you’re willing to model). Mirror the style seen in Anthropic.

– Prepare a repository layout for specs and proofs living alongside code. Establish a review rule: no proof is accepted without a human sign‑off on assumptions and property wording.

– Baseline KPIs: number of properties defined; proportion of target modules with at least one property; time from property proposal to first proof attempt.

Days 8–14: get the verification lane running

– Add a CI job that builds artefacts and triggers the verification lane; store proof artefacts and logs as build outputs. Keep it non‑gating. Surface the results in the same place developers read test and fuzz reports (CI/CD remains the hub).

A pre-investment technology review applies the same questions with a transaction attached.

– Use the model to draft initial proof scripts for the selected properties. Expect iteration. Track: proof attempts/day; proof success rate; time per successful proof; defects surfaced by proof failures vs tests.

Days 15–21: harden and expand

– Tighten assumptions where feasible and stabilise specs. Promote at least one property to “must‑pass” for a single module. Build a small library of reusable proof patterns and property templates.

– Start porting proofs across similar code paths—this is where LLMs shine by speeding up repetitive formal work, as evidenced by Anthropic.

– KPIs: proportion of attempted properties with stable proofs; number of unique defects found via proofs; reduction in flaky tests for verified paths (if any).

Days 22–30: make it policy, not a project

– Define a gating policy: which properties block merges, and under what assumptions. Keep the gate tight but small (one or two properties) to avoid grinding delivery to a halt.

– Publish dashboards: property coverage by module; proof pass/fail trends; defects discovered via proofs. Make the artefacts and assumptions auditable.

– Write contribution guidelines for adding new properties, updating assumptions, and reviewing proofs. Assign ownership.

What to do now

– Pick a candidate property today. If you handle untrusted inputs, start there. Re‑express one of your high‑value test assertions as a proof goal under explicit assumptions, mirroring the successful pattern reported by Anthropic.

– Treat the LLM as a junior proof engineer. Ask it to propose invariants and counterexamples; you decide what’s acceptable and what to tighten. This aligns with the evidence that models can produce useful formal artefacts and surface real bugs (Anthropic).

– Keep your toolchain pragmatic. If you already have proof assistants or model checking in‑house, integrate the model where it reduces toil. If you don’t, keep the verification lane isolated and measurable so it can earn its place.

– Hold yourself to clear KPIs: percentage of critical modules with at least one proven safety property; proof success rate; unique defects found by proofs; time‑to‑proof from property definition to accepted artefact.

The direction of travel is clear. The evidence from Anthropic suggests this isn’t a research curiosity any more; it’s a workable addition to production engineering. Start small, state assumptions, wire it into CI/CD, and let proofs carry the weight that tests can’t.