formally verified
Formally verified means that the correctness of a program or an AI component has been mathematically proven — not merely through testing, but through a proof that covers all possible inputs. In AI safety research, formal verification is considered one of the few methods that provides guarantees rather than mere probabilities.
When software is tested, a limited selection of cases is checked. If everything passes, the program is considered probably correct. With formal verification, it’s different: a mathematical proof shows that the program satisfies a defined property under all conceivable circumstances. There is no exception that happened not to show up in testing. The method originally comes from mathematics, where a theorem only holds once it has been proven — not when it turns out to be true in a thousand cases.
Guarantee instead of sampling
Tests have a structural problem: they can show that a bug is present, but can never prove that none exists. A test with a million inputs still leaves infinitely many cases open. In an autopilot or a medical diagnostic system, it is precisely this untested case that can turn out to be the decisive one.
Formal verification closes this gap. It is particularly suited to clearly defined properties: “This program never divides by zero.”, “The output is always between 0 and 1.”, “The robot never moves toward a person faster than 1 m/s.” Such assurances can be proven, not merely made probable.
That is why formal verification is especially valuable in safety-critical domains: in aviation, in nuclear power plants, and increasingly in AI research, where discussions center on how to ensure that a model never exceeds certain limits.
Proving instead of trying out
The foundation is a formal specification: a precise, mathematical description of what the program is supposed to do. Everyday language is not sufficient for this — “the system should be safe” is not a checkable statement. Instead, properties are formulated in a logical language, for example: “For every possible input x, the following holds: if x is greater than zero, then the output is positive.”
A proof assistant — a specialized program — then checks whether the code actually satisfies this property at all times. Well-known tools for this are called Coq, Isabelle, or Lean. They force the developer to make every step of the argument explicit. Gaps in the proof are flagged as errors, similar to syntax errors in ordinary code.
For simple programs, this is laborious but feasible. For large neural networks, i.e., the models behind modern AI systems, current methods still run up against limits: the number of possible states is so vast that complete proofs are computationally nearly impossible to produce. Researchers are therefore working on simplified partial proofs that at least provide guarantees for certain layers or outputs.
Where “formally verified” appears in practice
In everyday life, formal verification is usually invisibly embedded in systems where a crash is not an option. The onboard computer of the Ariane 5 rocket contained a bug in a type conversion — a kind of bug that formal verification could have ruled out. In the successor, parts of the code were in fact formally verified.
In the AI debate, the term comes up in connection with AI safety. Organizations such as DeepMind or the Alignment Forum discuss whether future AI systems must have formally verified safety properties before they are allowed to be deployed. The idea: a model whose behavior is mathematically proven to be correct would be more reliable than one that has merely been tested well.
The method also plays a major role in chip development. Intel and AMD use formal methods to ensure that their processors compute arithmetic correctly — a response to the Pentium FDIV bug of 1994, in which a computational error in the chip caused millions of dollars in recall costs. Since then, formal verification has become standard practice in the semiconductor industry for critical computing units.