FAQ.

What is formal verification?

Formal verification uses mathematics to prove that a program has a specified property. For example, a proof can show that optimized code behaves exactly like unoptimized code. It can also show that a production implementation matches a reference implementation on every input.

Tests and proofs both give feedback about correctness. As Dijkstra explained in 1969, testing can show that bugs exist, but cannot show that no bugs exist.[1] A proof can establish a property for all possible inputs. A test checks only a subset of those inputs.

Why does this matter?

In the near term, verification gives defenders an asymmetric advantage against cyberattacks. After a proof establishes a property, defenders do not need to keep increasing their effort as attackers gain more compute.

In the long term, verification offers a way to oversee increasingly capable models. A codebase can change completely over time. Reviewers can still retain a short list of intended changes to behavior and a proof that the code meets those requirements. This lets reviewers account for every change in behavior.

Theorem estimates that 95% of the machine code in nixpkgs could have proofs by the end of 2027 for about $134M. This estimate assumes that model capability on verification improves 4× faster than Epoch AI’s general trend.[7] For comparison, estimated global cybercrime damages total roughly $500B a year.[8]

What is the advantage over testing?

A test checks the inputs that you selected. A proof covers all inputs. Proofs also remain useful as code changes. Tests depend on implementation details, so a refactor can require you to rebuild the test suite that you trusted.

With verification, the theorem statement stays the same. A model can generate a new proof for the changed implementation. This lets you change code faster and use compute to establish correctness.

Some bugs occur too rarely for testing to find them. Certain cryptographic bugs occur in as few as 19 out of 2²⁵⁵ inputs. Random testing would need an enormous number of computers to find one within twenty years. That number exceeds the number of atoms in the solar system by more than 1,000×.[2]

Test coverage measures which parts of the code tests execute, but it is a weak signal of correctness. A study examined about 100 mature open-source Java systems. It found no meaningful relationship between test coverage and bug counts after release.[4]

What are the limits of a proof?

A proof only guarantees a specific claim about a program based on the specification, so it’s important to ensure that your specification matches your intent and scope. For example, a proof that an optimization preserves behavior says nothing about whether it made the program faster.

Similarly, security guarantees hold only under the threat model specified. For example, a proof may establish that an encryption program’s outputs do not reveal its secret key. However, if the threat model excludes timing attacks, the proof does not establish protection against them. An attacker could still infer information about the key from differences in execution time.

Why is verification not more common?

Verification requires substantial human effort. Only a small number of engineers with PhD-level expertise can do this reasoning-intensive work. Handwritten proofs typically contain 10–100× as many lines as the code they verify.[2]

Across projects such as seL4 and CompCert, teams verified a median of about 2,558 lines of code per person-year.[5] Verified software therefore requires much more code and 2–5× as much human effort.

Engineers mostly use verification where mistakes are very costly and development is slow, such as hardware design and cryptography. Tools are mature for small programs and formal proofs of mathematics. They are less mature for large software systems in production.

How does AI change verification?

AI can write code and construct proofs much faster than people. This reduces the human effort needed to produce verified software.

A specification can be much shorter than the code it describes. Instead of reviewing every line of AI-generated code, people can review those requirements. A proof assistant checks a proof that the generated code meets them. Verification therefore offers a way to oversee large amounts of generated code without reviewing each implementation manually.

In Theorem’s lf-lean project, AI produced verified translations of 97% of 1,276 textbook statements, over 350× faster than manual verification. The workflow automatically generated correctness specifications for the whole class of translation tasks. The need for human oversight therefore stayed constant as the number of tasks grew.[5]

What limits AI-driven verification?

Training data

The Stack v2 is a standard public collection of source code.[6] Formal verification languages account for only about 1 part in 10,000 of its volume, according to Theorem’s analysis.

Shared infrastructure

Verified software depends on other verified software. Today, each project resembles creating a new repository that contains the project and all its dependencies. Shared proofs can reduce this duplication and its cost.

Nearly 16,000 packages in nixpkgs depend on OpenSSL at runtime. Sharing one proof of OpenSSL across these packages costs roughly $14 per package that reuses it. Theorem estimates that verifying nixpkgs with shared proofs would cost about $6.4B. If each package separately verified its dependencies, the estimated cost would rise to about $190B.[7]

Proof assistant performance

Proof assistants still have substantial room for optimization. In Fiat Cryptography, checking a two-word example took about 14 seconds. Checking an eight-word example took about 20 hours. The projected time for a 17-word example exceeded four thousand millennia.[2]

What is a proof assistant?

A proof assistant, such as Lean or Rocq, lets you write theorems and proofs as source code. A theorem states the claim that you want to prove. When you compile a proof, the assistant mechanically checks whether the proof is valid.

You write proof code, examine the goals that remain, and continue until the assistant accepts the complete proof. If the proof compiles, it establishes the stated theorem. An expert does not need to review the proof itself.

Trust depends on a small proof-checking kernel, the part of the assistant that checks proofs. Trust does not depend on the person or model that wrote the proof. This separation lets the assistant accept AI-generated proofs without human review (the “de Bruijn criterion”; Gross, 2021).

Examples include CompCert, an optimizing C compiler,[3] and seL4, an operating system microkernel. Fiat Cryptography generates arithmetic code that ships in Google Chrome.[2]

What do specifications look like in practice?

Simple equivalence specifications provide most of the value. They state that two implementations behave the same. For example, an end-to-end fuzz tester could compare a production implementation with a reference implementation. The specification could require that the tester find no difference for any random seed. Writing these specifications does not require using a proof assistant.

Security work adds leakage specifications. These limit what an attacker can learn about the inputs. The production implementation must not let the attacker distinguish more about the inputs than the reference implementation does.

At the binary level, a few universal statements, such as “this program is memory safe,” provide most of the value. These statements are short enough for a person to review. Proving them still requires deep invariants and functional correctness.[7] Invariants are properties that remain true as the program runs. Functional correctness means that the program behaves as specified.