Good to see this happening, although aside from the memory-safety, thread-safety bit, how does it compare to SPARK[1], which I am currently using due to its leg

Good to see this happening, although aside from the memory-safety, thread-safety bit, how does it compare to SPARK[1], which I am currently using due to its legacy of being used for real-world applications for a couple of decades. SPARK has a verification toolset. I hope the collaboration between AdaCore and Ferrous Systems brings Rust closer to SPARK's current capabilities in producing high-integrity software. I didn't find a formal document from NIST listing what criteria have to be met to be put on this list other than the mention that "ISO/IEC/JTC 1/SC 22/WG 23 is working on"technical report (TR) 24772 Guidance to avoiding vulnerabilities in programming languages." [1] https://www.adacore.com/about-spark https://www.adacore.com/about-spark