Airbus has been been doing "codeless" development with Esterel products for quite a while. I put codeless in quotes, because I believe the tools to generate code at the end of the day - but it's not code that is written by humans, and it is generated based on formally verified models.

I believe this is what Airbus uses: http://www.esterel-technologies.com/products/scade-suite/

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

Very interesting! Trying to understand a bit better... does this mean that a human writes some logic, then it gets translated into a formally-verified model? Or these are pieces of verified code with strict combinatorial rules and the human does the composition?

"low code" is a thing apparently.