Proof Statistics
This page collects some numbers on the size and shape of things related to the seL4 correctness proof. See the SOSP paper on the publications page for more detailed data.
How big is seL4?
8,700 lines of C code plus 600 lines of ARM assembly code.
How much of it is verified?
7,500 lines of C code. We currently do not verify the assembly code and the boot code (1,200 lines).
How big is the proof?
All together 200,000 lines of Isabelle proof script. Manually written, machine checked. Roughly 3,500 A4 pages if printed out (a stack about half a meter high).
This is one of the largest formal proofs ever done. For comparison, the famous machine-checked proof of the four colour theorem is about 60,000 lines in the theorem prover. The only other proof that we know of that is larger, is from the Verisoft project (they report about 245,000 proof steps). Of course, in mathematics, the smaller the proof, the better it is considered to be :-)
How much work was it?
In total, design, documentation, implementation and verification of the seL4 kernel come to about 25-30 person years. This includes a lot of new research, new tools, and new libraries. If we were to do it again, we think it would be less than 10 person years.
As a comparison, an industry rule of thumb for software certification in the Common Criteria process at Evaluation Level 6 (which is not even the highest) is $10,000 per line of code. That means a traditional process would be around $87 Million for seL4 and would give less assurance. This means the verification cost was an order of magnitude less than estimated traditional certification.
How many bugs have you found?
We found 160 bugs in the C code in total. 16 of these were found during testing and internal student projects running the kernel before the C verification had started in earnest. 144 bugs were found during the C verification phase.