I’ll add that SPARK Ada allows this now, has commercial tooling from Adacore, and was field-prove in years of commercial deployments. https://en.m.wikipedia.or

I’ll add that SPARK Ada allows this now, has commercial tooling from Adacore, and was field-prove in years of commercial deployments. https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language) It builds on the Why3 platform which also supports Frama-C for the C language. IIRC, SPARK can be compiled to C for C-only, runtime targets as well.