Hi! I am writing down an explanation about Coq’s trust model and need some info about the trusted codebase. In particular:
- What is the size of the trusted code base?
- What steps been taken to assure it is bug-free? Manual code reviews? Paper proofs? etc.
- How many bugs were found in it?
This presentation is citing 18 KLOC and “1 critical bug per year”, but I would love to see more info.
I will appreciate any pointers and relevant information.
P.S. I am just interested in the kernel. Not parsing or extraction.