formal verification

Formal verification uses mathematical proofs on programs in order to ensure their properties. To quote from 1: "Complete formal verification is the only known way to guarantee that a system is free of programming errors"

{x > 0}  // true before 
x = x + 1 // C for increase by 1
{x > 1}  // true after (see the second note below)


  1. seL4: Formal Verification of an OS Kernel
  2. This is of course wrong if x == MAXINT, formal verification provides tools for catching such errors.
  3. Gotfail and a defence of purists: "And we had demonstrably the most reliable real time software ever written. After amassing several thousand implant-years, we measured a bug rate of less than one in 10,000 lines." The reader will note that were at least two errors with Phil responsible for 1!. Still typical industry figures are an order of magnitude or more higher which I claim in part was due to formal method and smart people.