<sup>*</sup>Equal contribution
Edit: On October 19, we added a proof-efficiency eval that shows that model performance on software verification doubled every two months between May and September.
AI systems are now sufficiently capable of formal verification that we can seriously contemplate a future in which all software is verified. What would it take to reach that future?
This post uses the nixpkgs bootstrapping chain as a blueprint for a verified software stack. Nix makes a good case study: it records the dependency chain behind every package, which can be followed from the bottom up, and it covers a significant share of the software running in production today, including critical infrastructure like glibc, OpenSSL, and curl. We estimate the cost and time needed to verify all of it. It’s within reach by the end of 2027: if models can be made to improve at verification much faster than they improve overall, 95% of nixpkgs’ machine code could be verified for about $134M. 1 For reference, global cybercrime damages are estimated at about $500B a year. Global Cybercrime Damages, GovAI, 2026, Kamile Lukosiute, John Halstead, and Luca Righetti.
Setup #
What does it mean to verify software?
Our goal is to verify massive amounts of software without being bottlenecked on human review, in a way that is useful in production. This means:
- Human review should scale with how complex the software’s intended behavior is, not with how much code there is.
- Bugs found during proving should be real bugs in the software, not artifacts of how we modeled it.
- We must handle real production systems, not simplified versions of them.
These requirements push us to verify programs at the binary level. Verifying binaries means that programs in any language, built with any toolchain, can be represented in the proof assistant. And because the binary is what actually runs, bugs found while proving it are real bugs.
Once we work at the binary level, broad verification becomes surprisingly cheap to specify. Abstractions are leaky, and optimized code strips out checks that are only unnecessary if the rest of the program is correct. So even a simple theorem like “this program is memory safe” can only be proved by establishing complex invariants and the functional correctness of its components.
As a result, a few universal statements like this one do most of the work. They are short enough for a human to review, even though proving them is not.
Bootstrapping from shared libraries #
Software is largely modular, so we can verify the whole Nix ecosystem iteratively and in parallel. 2 The median dynamically linked binary is about 30 KB. The median package’s runtime dependencies total about 250× its own machine code, and about 85% of packages depend on packages that, in aggregate, are more than 5× their own size. In all, nixpkgs holds about 150 GB of machine code in more than 120,000 binaries. Just 9 MB of shared libraries is the complete dependency set for two thirds of that code. 3 170 MB of shared libraries is the complete dependency set for 80% of the code, and 1.4 GB is the set for 90%. Prove those universal properties for these few libraries once, and most of the code can reuse the results.
Each binary’s verification job starts once its runtime dependencies are verified, and builds on their verified interfaces instead of reopening their implementations. Among the jobs ready to run, we prioritize libraries that block many programs.
Sharing is what makes this affordable. If every nixpkgs package verified its own runtime closure, the closures would total 4.4 TB, 30× the distinct machine code, and would cost about $190B at today’s rates instead of about $6.4B. OpenSSL alone sits in the runtime closure of nearly 16,000 packages; at today’s rates its proof would cost about $220K, or about $14 for each package that reuses it.
Modeling assumptions #
We give each binary one verification job, estimate its cost in dollars and in time, and add these up for the totals. Total cost is , where is the total hours of verification work, is the verification rate in KB per hour, and is the cost of verification per KB. Total time depends on the order of dependencies, how fast model capability grows, and how many jobs run in parallel.
Both the rate and how fast it is improving come from our proof-efficiency eval, which asks a model to verify 36 small C programs, each 0.5 to 2.5 KB of machine code. Across seven Anthropic and OpenAI models released between May and September 2026, verification speed doubled about every two months, from about 0.12 KB per hour for Opus 4.8 to between 0.6 and 0.9 KB per hour for the September models (Fig. 2). 4 Speed is KB verified per wall-clock hour, counting passing attempts only. Claude models ran in Claude Code with a 1M-token context; GPT-6 models ran in Codex. The fit is a least-squares line through log speed against release date. GPT-6 Luna passed fewer than 8 of 108 attempts and is excluded.
Our starting point is = 0.5 KB per hour, a little below the September models, and = $40 per KB. 5 Time and cost scale linearly with binary size. This holds on the small binaries we tested, and more than 90% of binaries are under 2 MB, not counting dependencies. We assume the measured trend holds, and capability on this task keeps doubling every two months. That is four times as fast as Epoch AI’s eight-month estimate for language models in general. 6 Algorithmic progress in language models, Epoch AI, 2024, Anson Ho et al.: the compute needed for a fixed level of performance halves every eight months (95% interval: 5 to 14 months). As capability grows, rises and falls by the same factor, so and the total cost shrink.
A budget of dollars a year pays for 7 8,760 is the number of hours in a year. jobs running in parallel on binaries that don’t depend on one another.
Cost and timing #
At $100M a year, 95% of the machine code would be verified by the end of 2027 and the last package about a year and a half in, for a total cost of about $134M. Fig. 3 shows the full schedule: when each package would be verified, and in what order.
Getting to work #
Getting there takes contributions from across the ecosystem. If you build software, tell us what you want to prove: bring us the end-to-end properties you care about, and we’ll help turn them into theorems about the software that actually runs. If you build frontier models, work with us to make them better at formal verification. If you build chips or proprietary platforms, publish complete specifications of the behavior software relies on. If you work on systems or formal verification, come work with us.
If you want to help us build a verified software stack, reach out.
Appendix: Data and modeling details #
The data comes from a single nixpkgs snapshot of the nixos-26.05 channel, taken on September 16, 2026, with machine code read from the binary cache. After deduplicating and keeping only x86 binaries, the snapshot holds 123,471 binaries in 28,650 packages: 153.7 GB of machine code. A binary’s size is the size of its .text section. Edges in the package graph are runtime references only.
In the schedule, a package is finished once its whole runtime closure is verified, and its value is discounted exponentially with a half-life of six months. A binary’s priority is the discounted value of every package whose closure contains it, per KB of those closures still unproved. Every package in nixpkgs carries the same value, so priority is roughly the number of packages a binary unblocks per KB left to prove.
Capability at time , in years from September 2026, is times the starting rate, where is the doubling time: two months, as measured in Fig. 2. Work that would take years at the starting rate then takes
years, with in years.
Theorem Blog, September 2026.
https://theorem.dev/blog/verified-software-stack/
@misc{theorem2026verifiedsoftwarestack,
title = {Bootstrapping the Verified Software Stack},
author = {Margaret von Ebers and Isabella Hampton and Harshikaa Agrawal and Luke Champine and Rajashree Agrawal and Jason Gross},
year = {2026},
month = {september},
howpublished = {Theorem Blog},
url = {https://theorem.dev/blog/verified-software-stack/}
}