5 ms·
The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the pr
by rzmmm 3mo ago
The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.
- jaggederest 3mo agoThere's an information theoretic aspect about generating a proof which is essentially not human readable from 4900 lines of spec. I wonder how much additional signal they're getting out beyond what's in that 4900 lines, and what's the percentage of noise in the 200k lines of proof?