We report on our experience using Haskell as an executable specifi-cation language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the mi-crokernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal ver-ification. The kernel comprises 8,700 lines of C code; the verifica-tion more than 150,000 lines of proof script.
展开▼
