4 ms·

It does not have to remain at stone level, and it can get legit certifications, too. Looking forward to it. A formally verified OS is a great step towards bett

• AlotOfReading 1y ago
  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
  • johnisgood 1y ago
    There is none in [0]. :P