Skip to main content

One post tagged with "Rust"

View All Tags

ยท 5 min read

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ย ๐Ÿ’Ž.