[nickpsecurity]

Let's not forget the security kernel in Guttman's cryptlib. It's like a lightweight variant of formal verification that justs makes sure things interface correctly.