Comment by lrvick

> the less your OS can do, apart from strictly hypervising guest operating systems, the safer you probably are

100% agreement here and I -would- take something tiny I can audit myself over something huge and formally verified if forced to choose. Thankfully I do not have to choose.

> AI lets us be more ambitious with verification

Exactly. For TCB code formal verification is a minimum, not sufficient, IMO. Too cheap these days to not have very complete test coverage, formal verification, risc0 execution proofs, seccomp tracing. For security critical code we should demand all of it now.