CakeML[0] is another formally verified compiler. Notably, unlike compcert, it is open source. The language it implements (an sml dialect) is high-level and ga

CakeML[0] 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. 0. https://github.com/CakeML/cakeml https://github.com/CakeML/cakeml