Formal Verification: The Ultimate Fitness Function

How to accelerate evolutionary search while building confidence in its results

The last three posts set up an arc toward understanding how our evolved natural world works in computing terms, so we can work toward deliberately designing an alternative structure that takes heavy advantage of AI. One of the important observations at the end of that sequence was that AI agents are importantly different from human scientists and engineers: an AI agent has source code that we can analyze in various ways. An expensive but reliable analysis by a trusted party can be distributed to many decision-makers using cryptography, but how can we realistically carry out such analysis about agents with complex source code?

This post is a proper debut for the technique of formal verification, one of the most common ingredients in my own research, which turns out to be a great solution to that last puzzle. It puts the “Guarantees” in the name of this blog. I am going to make the case that, when we take the long view on the evolution of intelligent life, formal verification could play a critical role, where integrating it into a transition to heavier reliance on AI can give us an improbable win-win: we can make evolution faster at developing technical innovations at the same time as achieving higher confidence that the process aligns with our objectives.

Roughly, formal verification is about mathematical proof about the correct behavior of programs. In contrast to testing, a proof can cover all possible situations a program finds itself in. The catch is that we have to decide which theorem or specification to prove about the program. If we prove it follows some rule that actually doesn’t match our true objectives, then we may actually be worse-off than before, with a false sense of security.

Introducing formal verification to a broader audience used to require quite some set-up, but these days I can say “it’s like how creators of foundation models are benchmarking them against writing mathematical proofs automatically (e.g. with AlphaProof), except I’m talking about showing correctness of programs rather than theorems in pure math.” I’m probably not the only specialist in formal methods who was surprised when it turned out to be useful to justify its interest and feasibility for realistic software by citing work in pure mathematics; usually the marketing strategy goes in the other direction!

I’ll save further more-technical details (of which there are many relevant categories) for future posts. My goal in this post is to explain the key role that formal verification can play in evolutionary search. I’ll start with a concrete example that is used in production code that you’re likely running to read this post. Then I’ll stand back to get philosophical about how the evolutionary process stretching back billions of years can get a fundamental upgrade using such methods. The following two posts will get more specific about using these ideas to solve variants of important problems in AI safety. A preview of the main claim is that formal verification unlocks a new kind of fitness function for evolutionary search, offering dramatically shorter feedback cycles than natural selection ever found or even than mainstream engineering today can pull off.

CryptOpt: Searching for Fast Cryptographic Code

Let me use a concrete example that combines evolutionary search and formal verification to write better code. Two research and open-source projects that I’ve been involved in are Fiat Cryptography (research paper, GitHub) and CryptOpt (research paper, GitHub). Fiat Cryptography is a domain-specific compiler: it turns programs in a high-level, more human-readable programming language into efficient code that CPUs can understand more directly. It is specialized to the domain of cryptography. What’s interesting about this compiler is that it is formally verified: we built a machine-checkable proof that it only produces code that computes the right mathematical functions. The fast code was more typically written manually by humans, who would sometimes make mistakes that had security consequences. The idea of automating that process with the strongest mathematical guarantees was compelling enough that now all major web browsers use Fiat Cryptography to build parts of their libraries for secure browsing.

However, the first versions of Fiat Cryptography bottomed out in popular programming languages like C and then called standard compilers to finish the work, creating assembly code (some of the lowest-level computer code that is long and easy to get wrong) that was significantly slower than what the best experts were writing by hand. That observation motivated us original authors of Fiat Cryptography to join new collaborators in building CryptOpt, which uses random program search to evaluate many potential programs and keep the fastest one.

We’re familiar with evolution operating on family trees of animals. Only animals that succeed at survival and reproduction propagate their genes into later generations. New individuals take on mixes of genes from their successful parents.

Evolutionary search through programs can work similarly, except now the population is of, in the case of CryptOpt, assembly programs. We measure fitness by running programs on the actual target hardware and measuring their performance. Only the fastest variants known at any given time “survive.” New program variants are generated by trying simple tweaks on prior champions, like reordering their instructions.

We have a very effective fitness function for evolutionary search, based on quick, focused performance benchmarking. (By the way, performance evaluation turns out to be easier in this domain than in general software engineering, thanks to wide adoption of well-motivated coding guidelines.) However, running quickly is only part of the story: we also want programs to get the right answers.

CryptOpt is designed to apply only behavior-preserving transformations to program variants, but those transformations could still contain bugs. To maintain the high standards of formal guarantees from Fiat Cryptography, we extended the latter with a new program-equivalence checker. Passed the original C-like program produced by Fiat Cryptography plus a champion assembly program produced by CryptOpt, this checker can establish that the two compute the same mathematical function. While we worry that such equivalence checking in general is undecidable (formally, no software could answer every equivalence question correctly), the equivalence checker in this case was carefully codesigned with the search procedure, so that valid programs should never fail checking. Also, the equivalence checker was itself formally verified (through nontrivial human proof-writing effort), so nothing about the evolutionary search process needs to be trusted. It is also no longer possible for bugs in standard C compilers to endanger correctness: the whole generation path, from whiteboard-level math to assembly language, is covered by one integrated proof in Rocq, and that path is effective enough that we even set some new performance records for particular cryptographic algorithms on particular hardware.

We started the CryptOpt project shortly before ChatGPT introduced the world to the potential of generative AI. I don’t think anyone has tried it yet, but there is a natural variant of CryptOpt that would use an LLM to suggest program variants. If we use the same kind of formally verified equivalence checker to vet every proposal, then we don’t need to trust the LLM, while still taking advantage of its creativity. Whatever crazy ideas the LLM comes up with, the formal verification guarantees that the ones it accepts are correct. The result is an appealing division of labor, between one partner (the LLM) that is creative and unreliable and another partner (the formal verification) that is by-the-books and doesn’t miss a single detail.

This recipe is a general one for accelerated evolutionary search for better artifacts that can be represented precisely on computers. It connects to the established research areas of superoptimization and program synthesis. The key point is that while natural evolution can take the whole lifetime of an animal to evaluate its fitness, formal methods allow up-front evaluation of individuals, considering how well they meet requirements in the infinite variety of “lives” they might lead. Let me now step back and put that advantage in context, within the progression from lifeless matter to intelligent people.

Stages of Evolution

Let’s consider five stages of evolution as a kind of staircase, leading up to one that depends critically on the approach I just explained. The grounding in subject matter very much outside computer science prepares us to see what fundamental algorithmic advantage formal verification can give to search processes, with applications to timely domains like AI safety. This sequencing is similar to Kurzweil’s epochs in The Singularity is Near, but I’m going to get into more geeky implementation detail.

Stage 1: Lifeless Matter

The universe is in a state that would strike us as very random. Things change from moment to moment, but there are not yet clear patterns. We don’t see anything going on that remotely deserves the name intelligence.

Stage 2: Natural Selection

Certain patterns that are able to perpetuate themselves have developed and started a virtuous cycle, through replicators like genes. Plans for organisms are copied and recombined across generations, with relatively small mutations. Individuals less fit to survive or reproduce naturally have their genes influence future generations less. However, there is a very slow feedback process to the distributed evolutionary algorithm that we can think of as running. The ground truth may be that an individual is relatively unfit in its environment, and yet that individual plods along for quite a while. There is only so much effective search we can expect with a “judge” of fitness (differential survival and reproduction) that most of us would not consider intelligent.

Stage 3: Sexual Selection and Signaling

Individuals start judging each other through sexual selection and signaling. Brains can judge the fitness of other brains and bodies, making decisions that influence the survival and reproduction of those they evaluate. The judging rules can even be “programmed” through culture, to adapt as the evolutionary landscape changes. Individuals learn to display costly signals to make themselves easier to evaluate. These signals allow a much quicker feedback loop for the distributed algorithm to measure fitness and act accordingly, as the time to when an individual can produce the right signal may be orders of magnitude sooner than the time until it encounters a “real-life situation” demanding the skill to be signaled. Still, as in software testing, a given combination of signals can still mask crucial flaws, but it is hard to do better without a good way to introspect into an individual’s “code.”

Stage 4: Humans Implementing AI Agents

Now we come to a fundamental transition in intelligence that has already occurred. It probably makes intuitive sense that explicit design by the best minds can produce better ideas than a largely “brute-force” evolutionary process, even if the latter has a head start of billions of years. We could even see explicit design of intelligence by other intelligence as an important cosmic milestone that should speed up the flow of history. Still, we should acknowledge that our deliberate intelligence sits inside an evolutionary context, with both individual and group selection. Descriptions of the next two stages should be interpreted in that light.

Here is where the state of practice is today (alongside the earlier modes of evolution, of course). Programmers (often with help from AI coding agents) develop new AI agents, thinking carefully about what competencies those agents should have. Testing can still be used (and is indeed the dominant method) to confirm how well new agents do against their creators’ goals. In theory, we can also analyze the code of agents to produce watertight arguments about their future behavior. However, carrying out this analysis on nontrivial code bases is difficult.

It’s difficult even within a tightly integrated engineering team, but another aspect of technological innovation today is teams that compete but also take inspiration from each other’s work. There is a high cost to adopting an idea from a competitor, as you need someone who is not much less expert than the inventor to go through the whole argument in favor of an idea. We could even imagine unscrupulous teams publishing ideas that they know are bad but that are designed to attract competitors to adopt them. It is very appealing to take advantage of low-cost cloning of as many copies of an agent as we want, but the due diligence is expensive with present mainstream methods.

Stage 5: Automated Search Backed by Formal Verification

Formal verification provides the missing ingredient. As a search process refines agents, it can generate mathematical proofs that they meet appropriate specifications. These proofs can cover all possible scenarios. They are also relatively easy for skeptical third parties to recheck, even if the proofs were hard to find. Those third parties can also delegate proof checking to well-resourced evaluators via cryptography. The result is a historically novel tool: a fitness function that can be evaluated almost instantly (via proof checking) but that covers every situation an agent might be asked to handle.

To make it work, we need to clear some apparently very challenging technical hurdles, like proper design of specifications (what does correctness or safety even mean for powerful AI agents?) and scaling of tools for finding proofs. I believe the prospects are good for sorting it all out, but details will have to wait for what I promise will be extensive coverage in future posts. Also, let me mention here that the burgeoning research area of verification for neural networks is related but encompasses a smaller scope, both (1) because we may want assurance in software that doesn’t use neural networks or still contains important other components and (2) because one very-relevant method is correct-by-construction software generation where we know a program is correct by virtue of how it was written, without a residual need to analyze the final source code.

Conclusion

My argument is roughly that formal verification can power a kind of have-your-cake-and-eat-it-too step forward in technological progress. Arguments around the future of AI often contrast work on capabilities and safety. Evolutionary search connected to formal methods can enhance capabilities by dramatically decreasing the feedback cycle for evaluating fitness of new variants, even in distributed systems where ideas are exchanged among parties that don’t trust each other. However, the technique can also enhance safety through low-cost and trustworthy checking that all variants meet appropriate specifications. Not only is there the potential to discover new levels of intelligence in much less time than it took natural evolution to discover ours, but we may even be able to do it in a way that guarantees those new intelligences agree with us in important dimensions.

There are a lot of details to get right, to reduce this idea to practice. I will cover many of them in future posts. To start with, let’s get one step more concrete by considering (in the next two posts) two common concerns in AI safety and seeing how this paradigm can help address them, starting with recursive self-improvement.