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)

References:

- seL4: Formal Verification of an OS Kernel
- This is of course wrong if x == MAXINT, formal verification provides tools for catching such errors.
- 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.