I am just starting out with the ironclad kernel and the gloire OS built on top of it [1,2]. From the web page:

  "Ironclad is a formally verified, real-time capable, UNIX-like operating system kernel for general-purpose and embedded uses. It is written in SPARK and Ada, and is comprised of 100% free software."

I recall AdaCore working with Ferrous Systems a while back. Did anything come of it for rust? I believe one of the non-starters is rust does not have a formal standards specification like C, Common Lisp, or other PLs. It's hard to develop formal verification systems for a moving target.

SPARK has formal verification tools and a legacy of high-integrity applications. The Ironclad kernel is progressing towards a substantially, formally verified kernel written in SPARK. Gloire is an OS implemented on top of Ironclad for PoC.

I have sort of given up on rust, because I just don't find it enjoyable. I am working with Zig. This would be a good direction for Zig to take. Glad to see the effort here. I'll have to check it out a bit more.

[1] https://ironclad.nongnu.org/

[2] https://github.com/Ironclad-Project/Gloire?tab=readme-ov-fil...