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ย ๐.