We are diversifying ourselves to apply formal verification on 3️⃣ new languages with Solidity, Rust, and TypeScript. In this article we describe our approach. For these three languages, we translate the code to the proof system 🐓 Coq. We generate the cleanest 🧼 possible output to simplify the formal verification 📐 effort that comes after.
Formal verification is a way to ensure that a program follows its specification in 💯% of cases thanks to the use of mathematical methods. It removes far more bugs and security issues than testing, and is necessary to deliver software of the highest quality 💎.