Formal Verification

Normally, software is checked through testing. You try out a few inputs and see whether the result is correct. This finds many errors, but never all of them: only ever a tiny fraction of all conceivable cases gets tested. Formal verification works differently. You write down precisely what the program is supposed to accomplish, and then prove mathematically that it always does so. The proof then holds for every possible input, not just the ones tried out. The difference is like that between twenty worked examples and a proof in mathematics.

Why it matters

Some errors simply cannot be allowed to happen. The control software of an airplane, the brakes of a train, a pacemaker: here, a crash costs human lives. It’s also expensive with processors. A computational error in a chip can’t be fixed with an update after production, only through a recall.

In cryptography the situation is similar. An encryption program can work correctly for 99.9 percent of inputs and still be unusable. Attackers look for exactly the one case that doesn’t work. Testing hardly helps against that, but a proof does.

Since AI systems have started making important decisions, the question is being asked anew. A language model itself cannot be formally verified, since it is too large and too imprecisely defined. But you can prove the software surrounding it, the software that monitors and constrains the model.

How it works

The first step is the specification. It describes, in a precise, mathematical language, what should hold. For example: the result of this sorting function is always ordered ascending and contains exactly the same elements as the input. This step is often the hardest, because only here do you notice how unclear your own requirements actually were.

Then comes the proof. For this there are programs called proof assistants, such as Coq, Isabelle, or Lean. The human provides the proof idea, and the program checks every step for gaps. It accepts nothing that doesn’t actually follow.

For simpler properties, it can also be done automatically. A model checker systematically searches through all reachable states of a system and reports whenever one of them violates the rule. Such tools find errors that humans overlook, because they stubbornly go through every combination.

The effort is the price. For a proven program, you easily need ten times the work compared to normal code. That’s why nobody verifies an entire app, only the critical core.

Where you encounter the term

Intel and AMD have been using formal verification in chip development for decades. The trigger was a computational error in a Pentium processor from 1994, which cost Intel a nine-figure sum. Today, every computational unit is mathematically checked before production.

Well-known examples from software are the operating system kernel seL4 and the C compiler CompCert. Both are fully proven and are used where regulatory authorities demand hard evidence, for instance in aviation.

In cryptocurrency news, the term comes up in connection with smart contracts. These are programs that automatically manage money. Because errors there lead directly to losses, some projects have their code formally verified and advertise this as a security feature. However, a proof only covers what is stated in the specification. If the requirement is formulated incorrectly, the proof is worthless too.