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.
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/sourc...
[1] https://github.com/seL4/l4v