[tptacek]

Honestly, I don't much care about the formal verification of L4; it's the L4 design and implementation strategy that I find compelling.