A roadmap for massively accelerating software verification

Theorem makes software verification cheap enough to scale.

Theorem makes software verification cheap enough to scale.

Software security today is largely reactive: we search for bugs, patch what we find, and repeat. Doing this with increasingly better models is useful for us as defenders, but it also means that hardening software against today’s adversaries is not a durable strategy against tomorrow’s. More capable models will find bugs that have survived years of testing and scrutiny.1 1 In 2026, Anthropic’s Claude Mythos Preview found a 16-year-old memory-safety bug in FFmpeg’s H.264 decoder. It’s one of the most heavily fuzzed codebases in the world, and the line that automated testing had executed five million times without catching it. The same effort surfaced a 27-year-old remotely triggerable crash in OpenBSD. Anthropic, “Project Glasswing,” April 2026. Each new adversary just needs to be smart enough to find one rare bug, while we have to spend increasingly more resources hoping to find as many as possible.

Formal verification has different, asymmetric economics. For properties we can formalize, a proof establishes claims about the entire modeled behavior of a program, and holds against the entire future army of smarter models. Agents will write these proofs for us, and because the proofs are machine-checkable, we never have to trust the agent — only the theorem it proved and the checker that checked it. We believe that verified software engineering will enable us to take on projects we could never have responsibly trusted before.

Verification provides stronger guarantees than testing alone. We’re bringing those guarantees to critical software: from the sandboxes agents run in, to compilers like GCC, and even the Linux kernel.

The verification frontier

Theorem’s mission is to make strong, machine-checkable guarantees about software cheap enough to apply by default. Today, that means moving the Pareto frontier of cost and capability for formal verification: make harder verification problems solvable, and make problems we can already solve dramatically cheaper.

Very few practical software systems have historically been formally verified, as producing proofs for large systems has required enormous amounts of rare expert labor. Under our paradigm, we can roughly define the cost of an agentic verification task as

tokens per proof × cost per token.

General model progress drives down the cost per token. We then do targeted RL training on verification, significantly reducing the tokens required to get to a successful proof. Both of those are the cost of finding a proof. There is a separate cost to stating the theorem itself — what the code should do, in a form a human can review — but we can reuse these specifications and semantics for later projects.

So we build reinforcement learning environments for verification, and use them to get frontier models better at exactly the skills our work depends on. Formal verification is a great substrate for RL because it provides rich, machine-checkable feedback; the structure of proofs lets us train models to reason about claims over whole classes of inputs rather than individual examples.

Using measurements from our verification of small projects, we’ve begun making rough estimates of what it would cost to verify much larger, critical projects.

We acknowledge some uncertainty about the domain shift from small to large programs, but we expect the core skills of good proof engineering, like choosing useful abstractions and invariants, decomposing large goals, or managing long proof horizons, to transfer as scale increases. We will update these extrapolations over time as we verify increasingly larger systems.

So why start verifying software now? It’s expensive, but it will get cheaper faster as we do more real work, and we only benefit by moving quickly on important targets.

Mapping our trajectory

We invest in infrastructure today that will reduce the marginal cost of verification tomorrow. That means choosing projects with two returns: they should deliver safety now, and create a flywheel internally.

First, we verify critical infrastructure that models themselves rely on. As models are aggressively optimized against their training environments, the evaluation and containment layer, including graders or sandboxes, becomes especially critical for security. We developed the practice of verifying against reward-hacking on our own grader for our RL environments.

In July, the world received a warning shot when agents being evaluated breached third-party systems.2 2 OpenAI, “Safety and alignment in an era of long-horizon models” (July 20, 2026) and “OpenAI and Hugging Face partner to address security incident during model evaluation” (July 21, 2026); Anthropic, “Investigating three real-world incidents in our cybersecurity evaluations” (July 30, 2026); OpenAI, “The Hugging Face incident and the road ahead” (Aug. 26, 2026). See also the controlled escape exercise in Anthropic’s Claude Mythos Preview system card (April 7, 2026). We’re responding to this right now, already verifying sandboxes and inference stacks with guarantees about isolation, access control, and model-weight security. Our sandboxing one-pager is here.

In parallel, we verify compilers. We want to verify down to the binary level to cover the entire attack surface.3 3 Thompson, “Reflections on Trusting Trust,” CACM 27(8), 1984. Reasoning about machine code, however, is expensive and unnatural for models, in part because source code contains abstractions that make programs much easier to reason about. If we can prove the connection between source programs and their machine behavior once, we save by reusing it across every downstream program. When we verify major toolchains such as GCC and Clang, we harden the whole ecosystem, and it becomes one of our largest multipliers.

Once that substrate exists, increasingly large and critical systems become affordable verification targets. Now we seed the ecosystem.

The projects in our sights for the near term may change, but each was chosen for the initial roadmap because it provides us something the others don’t. The Linux kernel is a natural pair to every sandbox we verify, because an isolation guarantee proved against a sandbox is only as strong as the kernel it runs on. Chromium is a huge attack surface and something most people touch every day, and Google is piloting bi-weekly patching to keep up with the bugs its own models find.4 4 Anthropic’s Frontier Red Team reported that Claude Mythos Preview found and exploited vulnerabilities in every major web browser. In one case, Mythos chained four vulnerabilities into a JIT heap spray that escaped both the renderer and OS sandboxes. The browser exploits were unpatched at publication and are held under cryptographic commitment (“Assessing Claude Mythos Preview’s cybersecurity capabilities,” April 7, 2026). Google separately reported fixing 1,072 security bugs in Chrome 149 and 150, both released in June 2026 — more than the 1,036 fixed across the previous 23 releases over two years. They attributed the surge to their own LLM-driven pipeline, and are piloting twice-weekly security updates (Google Security Blog, July 30, 2026; TechCrunch, same date). Google’s monorepo is critical for how we confront scale continuously. Much of the historical cost of verified software comes from keeping it verified with changes.5 5 seL4’s team reported 1.5–2 person-years to re-verify a single cross-cutting feature. Klein et al., “seL4: Formal Verification of an OS Kernel,” SOSP 2009.

From each of these projects, we get reusable specifications, formal semantics, libraries, theorem patterns, worked examples, and new training environments for the next generation of proof models. Our later projects will inherit an increasingly rich world of formalized infrastructure produced by earlier ones.

Finally, we make proof checking fast. Proof discovery may require large amounts of inference compute, but proof checking should not. As proof production scales, we can improve the performance of proof checkers and kernels by applying verified optimizations to the verification machinery itself.

Precision that scales with generation

Near term, this is an ambitious proactive-cybersecurity program: spend finite capital now to harden important software before increasingly capable models find the next generation of vulnerabilities in it.

It happens that the infrastructure this requires opens up something bigger. We envision a world where people can push into the unknown, the ambitious, the too complex for humans to independently reproduce and inspect. Verification provides secure footing through robust feedback at the frontier of hard problems and imaginative solutions. The ceiling on what we can responsibly build stops being what we can review, and becomes what we can prove.

We are in an unusually malleable period where agents can increasingly rebuild the software stack. The choices we make now will solidify into the defaults of everything built afterward. Move fast enough, and verification scales alongside generation, preventing the vulnerabilities that would otherwise compound quietly into the foundations, and enabling software more ambitious than anything we could responsibly trust before. These are our first steps towards that future.