[daveasdf]

The prover has a bug (most proofs are done automatically).

Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers).

You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.