Hello everyone, is there any formally verified Haskell compiler that you know of ? As far as I understand, the cardano-node source code itself is written with formal methods in mind, which makes it formally verifiable. However, unless using a certified compiler like CompCert for the C language, you won’t get formally verifiable machine code, will you ?