We make here a general presentation about how the formal verification of smart contracts works by explaining:
In this blog post, we continue our presentation about our formal verification tool for ◼️ Noir programs coq-of-noir. Noir is a Rust-like language to write programs designed to run efficiently in zero-knowledge environments. It has a growing popularity and a focus on providing optimized libraries for common needs, such as a base64 library using 🧠 field arithmetic that we use in this series of blog posts.
Here we present the details of our semantic rules to show that a Noir program has an expected behavior for any possible parameters. We focus, in particular, on our memory-handling approach and the definition of loops.
In this series of blog posts, we present our development of a formal verification tool for the ◼️ Noir smart contract language. It is particularly suited to writing zero-knowledge applications, providing primitive constructs such as a Field type to write programs that run efficiently as circuits. Having a formal verification for Noir enables the development of applications holding a large amount of money in this language, as it ensures that the code is correct with a mathematical level of certainty.
In this first post, we present how we translate Noir code to the 🐓 Coq proof system. We explore a translation after monomorphization and then at the HIR level. Note that we are interested in verifying programs written in Noir. The verification of the Noir compiler itself is a separated topic.
All our code is available as open-source on github.com/formal-land/coq-of-noir, and you are welcome to use it. We also provide all-included audit services to formally verify your smart contracts using coq-of-noir.