Standard ML Formal Verification Projects
CakeML: A Verified Implementation of MLProject mention: A Proven Correct C Compiler (Used by Airbus) | news.ycombinator.com | 2021-06-26
CakeML is another formally verified compiler. Notably, unlike compcert, it is open source.
The language it implements (an sml dialect) is high-level and garbage collected, meaning that it is not usable in all of the same domains, but work is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language.
Are you hiring? Post a new remote job listing for free.