Bootstrapping the Verified Software Stack

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?

In this post, we use the nixpkgs bootstrapping chain as a blueprint for a verified software stack. Nix is a good target for this case study: it records the chain of dependencies behind every package, which we can follow from the bottom up, and it holds a significant fraction of the software deployed in production systems today, including critical infrastructure such as glibc, OpenSSL, and curl. We model what it would cost, and how long it would take, to verify all of it. We think this is within reach by the end of 2027: if we can make models get better at verification much faster than they are getting better overall, 95% of nixpkgs’ machine code could be verified for about $134M.1 1 For reference, global cybercrime damages are estimated at about $500B a year. Kamile Lukosiute, John Halstead, and Luca Righetti, Global Cybercrime Damages, GovAI, 2026.

Our 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.

The order of work

We can tackle the whole Nix ecosystem iteratively and in parallel because software is generally modular.2 2 The median dynamically-linked binary is about 30 KB. For the median package, its runtime dependencies total about 250× its own machine code, and about 85% of packages depend on packages over 5× larger in aggregate than themselves. In all, nixpkgs holds about 150 GB of machine code in over 120,000 binaries. Of that, 9 MB of shared libraries is the complete dependency set for two thirds of the code.3 3 170 MB of shared libraries is the complete dependency set for 80% of the code, and 1.4 GB for 90%. Proving those universal properties for these few libraries, once, would establish facts about them that most of the code could reuse.

This orders our work. A binary’s verification job will start once its runtime dependencies have been verified, and will build on their verified interfaces rather than reopening their implementations. Among the jobs ready to start, we will roughly prioritize libraries that block many programs.

Without sharing, the cost would be far higher: if every nixpkgs package verified its own runtime closure, the closures would total 4.4 TB, or 30× the distinct machine code, and would cost about $190B at today’s rates. Sharing avoids this. OpenSSL alone sits in the runtime closure of nearly 16,000 packages; its proof would cost about $220K, or about $14 per package that reuses it.

Modeling assumptions

We estimate what each binary would cost in dollars and in time, with one verification job per binary, and add these up to get the totals. We model the total cost as $CV \times H$, where $H$ is the total hours of verification work, $V$ is the rate of verification in KB per hour, and $C$ is the cost of verification per KB. The total time would depend on the order of dependencies, how fast model capability grows, and how many jobs would run in parallel.

We estimate that we can verify $V$ = 0.5 KB per hour, at a cost of $C$ = $40 per KB.4 4 Time and cost scale linearly with binary size. We found this to be true on small binaries, and over 90% of binaries are under 2 MB when dependencies are ignored. These rates come from internal measurements, and we will revisit them as we verify larger systems. We ground them against two public efforts: the OpenAI Navier–Stokes proof ran at about twice our speed, and a recent verification of the xv6 kernel ran about 23× slower (see the appendix).

We assume that models will continue to improve. We take Epoch AI’s estimate for language models, where general capabilities double every eight months,5 5 Anson Ho et al., Algorithmic progress in language models, Epoch AI, 2024: the compute for a fixed level of performance halves every eight months (95% interval: 5 to 14 months). and scale it by a multiplier for this task. We expect reinforcement learning to push that multiplier above one. As capability grows, $V$ would rise and $C$ would fall by the same factor, so $H$ and the total cost would shrink.

A budget of $B$ dollars a year would pay for $N = B / (8{,}760 \cdot CV)$6 6 8,760: the number of hours in a year. jobs running in parallel on binaries that do not depend on one another.

Cost and timing

Under these assumptions, with a budget of $100M a year and model capability doubling at its current rate of once every eight months, the last package would be verified after about five years, at a total cost of about $404M. Fig. 2 shows the resulting schedule: when each package would be verified, and in what order.

Because most binaries are small and many do not depend on one another, at first a larger budget would allow more jobs to run at once, which would speed us up. However, nixpkgs has a long tail of large binaries: a dozen or so are over 100 MB. Past about $80M a year, or about 450 jobs at once, the extra jobs would have nothing left to work on while these finish.

We’re confident that models can get a lot better on this task through targeted training. If we can improve model capability at a rate four times as fast as our current estimate, doubling every two months, 95% of the machine code would be verified by the end of 2027, at a total cost of about $134M.

Getting to work

Getting there will require different contributions 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 will 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 take part in our future, reach out.

Appendix: Data and modeling details

The data is one snapshot of nixpkgs, taken 2026-09-16 from the nixos-26.05 channel, with machine code read from the binary cache. After deduplicating binaries, and keeping only x86 binaries, the snapshot is 123,471 binaries in 28,650 packages, 153.7 GB of machine code. A binary’s size in KB is the size of its .text section. The package graph’s edges are runtime references only.

Each rate traces to one of these sources:

• Baseline, 1×. Internal measurements suggest about 0.5 KB/hr (about 500 bytes/hr) using about 1 million tokens per KB. At frontier-model rates of about $40 per million tokens, that is $40/KB.
• xv6, 1/23×. Verifying the ≈40 KB xv6 teaching operating system (Kaashoek and Zeldovich, Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents, 2026) took, by our accounting, $1,600 and 77 days. That is $40/KB at about 22 bytes/hr, or about 46 hours per KB, 23× slower than baseline. Because our model ties cost to time, it would price work at that speed at about $920/KB, so we use xv6 as a check on speed only.
• Navier–Stokes, 2×. The recent Navier–Stokes proof had an internal OpenAI model writing about 600,000 lines of Lean in 17 hours, or about 35,000 lines/hr. Internal measurements put transcript length during proving at roughly 3.5× the final proof’s token count. At about 10 tokens per line of proof, 1 million tokens of transcript yields a bit under 30,000 lines. The implied rate is about 1 KB/hr, an extrapolation from mathematical formalization to software verification.

Neither public effort measures our task directly: the Navier–Stokes proof formalizes mathematics rather than software, and the xv6 verification used older models than ours. We expect some transfer from formalizing mathematics to verifying software, but they are not the same skill.

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. In nixpkgs every package carries the same value, so this is roughly how many packages a binary unblocks per KB left to prove.

Capability at time $t$ is $2^{mt/\tau}$ times today’s, where $\tau$ is eight months, Epoch AI’s estimate, and $m$ is the multiplier for this task. Work that would take $u$ years at today’s rate then takes

years, $\tau$ in years. The atlas uses $m = 1$.