No idea if any others are closer to that ideal, but MirageOS unikernel (OCaml) offers nods in that direction: "Possible to formally verify critical components"

No idea if any others are closer to that ideal, but MirageOS unikernel (OCaml) offers nods in that direction: "Possible to formally verify critical components" https://www.cs.williams.edu/~cs432/osco/01-whit.pdf https://www.cs.williams.edu/~cs432/osco/01-whit.pdf "As part of our mission to build robust and secure systems, we strive to support technology that roots its design in the field of formal methods" has a TCP stack manually derived from a formal model https://tarides.com/blog/2024-01-24-mirageos-designing-a-more-resilient-networking-stack-with-tcp/ https://tarides.com/blog/2024-01-24-mirageos-designing-a-mor...