formal verification
Formal verification is the practice of mathematically proving that a piece of software is correct, rather than merely testing it on a lot of inputs and hoping. Testing can show that bugs are present, but it can never show that none remain — you cannot try every possible input. A proof is different: like proving a theorem in geometry, it establishes that for all possible inputs the program behaves exactly as its precise specification says. For something as critical and trusted as a kernel, that difference is enormous.
It works by writing a precise mathematical specification of what the code should do, then using a proof assistant (a tool that checks logical steps with no gaps) to demonstrate, step by rigorous step, that the actual implementation always meets that specification. The landmark result is seL4, a microkernel whose C implementation was formally proven to match its specification and to be free of whole classes of bugs — no crashes from bad memory access, no buffer overflows, correct enforcement of its isolation guarantees. This is part of why the microkernel idea has had a resurgence: a microkernel is small enough (tens of thousands of lines) that proving it correct is actually feasible, whereas proving a multi-million-line monolithic kernel correct is far beyond reach today.
The honest limits matter a great deal. A proof only guarantees what the specification says, so if the specification itself is wrong or incomplete, the proven-correct code can still do the wrong thing — the bug just moves into the spec. Proofs also rest on assumptions (that the compiler, the hardware, and the proof tool are themselves correct), and they are extraordinarily labour-intensive, which is exactly why verified kernels are tiny and rare. Formal verification raises assurance dramatically; it does not deliver absolute, assumption-free certainty.
Engineers building a drone want certainty that one onboard component cannot read another's memory. They run their critical tasks on seL4, whose isolation properties are mathematically proven. No amount of testing could give that assurance for every input; the proof covers all of them at once — subject, honestly, to the spec and the hardware being as assumed.
A proof covers all inputs at once; testing can only sample some of them.
Proven correct means correct against the specification — not absolutely safe. If the spec is wrong, or the compiler, hardware, or proof tool is flawed, the guarantee can still fail. The bug moves to the assumptions, it does not vanish.