No mention of starting with a design specification & then tied to formal verification the whole way?

It sounds interesting and a step forward (never heard of library Os itll now), but why won't this run into hundreds of the same security bugs that plague Windows if it's not spec'd and verified?

People seem to believe writing things in rust means it's correct.