That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0

That really depends on what formal verification means in context. I don't see any interesting specifications in the repo, just basic stuff like this MD5 spec [0] that doesn't verify whether the MD5 implementation is correct. This is one of the areas where formal verification is listed as completed/gold level. It's common for the interesting OS proofs to take more code than the kernel itself. Take a look at the seL4 proofs [1], or those for CertiKOS as examples. If you're actually interested in alternative OSes in memory safe languages, you might like TockOS, which is more production-ready at this point. Formal verification work of the isolation model is still ongoing, because it's difficult work. [0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/source/cryptography/cryptography-md5.ads https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc... [1] https://github.com/seL4/l4v https://github.com/seL4/l4v