by Quentin Ochem – Sep 26, 2024. At AdaCore, we’re in the business of supporting people who develop high-integrity software, in particular for embedded systems. In terms of programming languages, this means supporting the most commonly found candidates, which in 2024 include C/C++, Ada/SPARK, and…
Might be relevant to mention that Rust has formal verification methods available as well, similar to SPARK, but also optional. One that looks pretty appealing is this one: https://verus-lang.github.io/verus/guide/overview.html