[nextos]

Maybe some more practical and less costly formal verification?

There are some signs Rust is heading in this direction.

Efforts like Dafny are also pretty interesting, but still far from mainstream.

I think a large codebase (20-40 KLOC) is about the maximum one can routinely verify in Dafny before stuff gets too hard. And coding speed is pretty slow.