From 2e5e5d05c6a9f0851fdf2b019ec5138191be6f18 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Tue, 10 Dec 2024 18:58:06 +0100 Subject: [PATCH] Update README.md --- README.md | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index a2d70299d3..a6cf5867fa 100644 --- a/README.md +++ b/README.md @@ -2,11 +2,21 @@ Noir is a Domain Specific Language for SNARK proving systems. With `coq-of-noir`, we provide an **affordable way to formally verify smart contracts written in Noir**. We rely on the well-known proof assistant [Coq](https://coq.inria.fr/) for the verification work as well proof techniques developed for [coq-of-rust](https://github.com/formal-land/coq-of-rust) and [coq-of-solidity](https://github.com/formal-land/coq-of-solidity). -## Status +## 🏎️ Run -This is still a work in progress. Contact us at [contact@formal.land](mailto:contact@formal.land) or by direct message on our [X account](https://x.com/FormalLand) if you are interested. +Follow what we do in our CI file [coq.yml](.github/workflows/coq.yml). Sorry for not having the time to provide more explanations! -## Goal and Vision +## ✅ What Works + +The following steps work: + +- A generated translation of the `base64` library of Noir to Coq in a code that compiles; we should thus support a large part of the Noir language. +- Semantics rules to reason on code like the above together with a proof strategy. This should already cover most of the Noir language. +- A formally verified functional specification of one of the functions with a loop from the `base64` library, exercising mutations and array access. We consider this to be our main test to see that `coq-of-noir` can work on non-trivial examples. + +Note that the proof process is still very verbose, and this tool is still a work in progress. Contact us at [contact@formal.land](mailto:contact@formal.land) or by direct message on our [X account](https://x.com/FormalLand) if you are interested. + +## 🔭 Goal and Vision The goal is to enable each team developing critical applications (meaning handling user money) to verify the correctness of their code with the higest degree of certainty thanks to **formal verification**. @@ -20,13 +30,13 @@ Our initial target is to verify a part of the [base64](https://github.com/noir-l _If you have a Noir project that you want to formally verify, either start using `coq-of-noir` or contact us!_ -## Blog posts +## 📚 Blog posts Here are some blog posts featuring this tool: - [◼️ A formal verification tool for Noir – 1](https://formal.land/blog/2024/11/01/tool-for-noir-1) - [◼️ A formal verification tool for Noir – 2](https://formal.land/blog/2024/11/15/tool-for-noir-2) -## License +## ⚖️ License -`coq-of-noir` is free and open source. It is distributed under a dual license. (MIT/APACHE) The translation phase is based on the code of the Noir compiler to maximize code reuse. +`coq-of-noir` is free and **open source**. It is distributed under a dual license. (MIT/APACHE) The translation phase is based on the code of the Noir compiler to maximize code reuse.