Yes they generate c code which is compiled. I don't know if the model is formally verified, but the whole toolchain from esterel, including the library blocks are certified (aicraft, automitive, industrial and train safety levels)

It does not mean that any software done with this tools is thus certified, you need to apply the safety methodology to certify it