To formally verify Rust programs, we are building coq-of-rust, a translator from Rustย ๐ฆ code to the proof system Coqย ๐. We generate Coq code that is as similar as possible to the original Rust code, so that the user can easily understand the generated code and write proofs about it. In this blog post, we explain how we are representing side effects in Coq.
4 posts tagged with "Coq"
View All TagsRepresentation of Rust methods in Coq
With our project coq-of-rust we aim to translate high-level Rust code to similar-looking Coq code, to formally verify Rust programs. One of the important constructs in the Rust language is the method syntax. In this post, we present our technique to translate Rust methods using type-classes in Coq.
Status update on the verification of Tezos
Here we give an update on our verification effort on the protocol of Tezos. We add the marks:
- โ for "rather done"
- ๐ for "partially done"
- โ for "most is yet to do"
On the website of project, we also automatically generates pages such as Compare to follow the status of the tasks.
Make Tezos the first formally verified cryptocurrency
Our primary goal at Formalย Landย ๐ฒ is to make Tezos the first crypto-currency with a formally verified implementation. With formal verification, thanks to mathematical methods, we can check that a program behaves as expected for all possible inputs. Formal verification goes beyond what testing can do, as testing can only handle a finite amount of cases. That is critical as cryptocurrencies hold a large amount of money (around $3B for Tezos today). The current result of our verification project is available on nomadic-labs.gitlab.io/coq-tezos-of-ocaml. Formal verification is also key to allowing Tezos to evolve constantly in a safe and backward compatible manner.