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.
Looking forward to it. A formally verified OS is a great step towards better security.