Formally proving tiny bits of qemu using Frama-C
Formal verification of software proves that the software is mathematically correct with respect to its specification. Frama-C is an open source modular framework for formal verification of programs written in C.