Formally Verified Arbitrum Stylus Verifier

[clarus]

We propose a translation of the Solidity smart contract for the Noir verifier in Rust in a way that is 100% safe and maintainable. For what we will:

• Keep a Rust representation of the contract that follows the structure of the Solidity code.
• Formally verify that the two are equivalent for any inputs.

Motivation

Maintaining several code bases can be challenging. In addition, verifiers are one of the most critical piece of software for a zero-knowledge systems so formal verification is considered as a requirement, for example by Vitalik, to use such systems at scale.

This is why we want to develop a Rust verifier that is formally verified as being equivalent to the original Solidity one. Note that we will not verify the original contract. But our translation will benefit from the same level of security as the Solidity contract. In addition, in case of a fix or evolution on the original contract, we will quickly propagate these changes on the Arbitrum Stylus version as we plan to follow the same code structure, and can easily check that all changes have been correctly propagated.

Methodology

We will rewrite the contract in Rust using the Alloy libraries (implementing U256 and all the data structures of the EVM), looking at the intermediate Yul code generated by solc, the Solidity compiler. This first rewriting may be done by hand or with the help of AI. We have experience in representing Solidity code in identical Rust code thanks to our project Oxidefier, a compiler from Solidity to Rust. Note that for this project we will make the translation more manually in order to have a more optimized output.

Then we will translate both the Solidity and Rust version in the Rocq theorem prover using coq-of-solidity and coq-of-rust to formally verify that the two behavce exactly the same, for any possible inputs.

In addition, we will run unit-tests, in particular to benchmark the rewriting of the code. As Arbitrum Stylus provides the same pre-compiles as the EVM we will also use them to implement the elliptic curve operations.

Timeline and Deliverables

The milestones are:

1. Month 1: Convert all the Solidity smart contract to Rust following a similar style, running benchmarks (we do not care about correctness yet).
2. Month 2: Formally verify that the two are equivalent. Although formal verification is generally complex, checking for equality can be much simpler, especially if the two programs follow the same structure.
3. Month 3: Clean everything up, document, and fix corner cases that were missing.

We can also run our project Oxidefier that is a compiler from Solidity to Rust, to get a baseline in terms of performance. In case the difference of speed is negligeable, we will drop our manual translation and prove equivalent the generated translation, what would be straightforward given that the translation is straighforward.

Team

The Formal Land will work on this project, with either Guillaume Claret (me) or the company's members. As relevant experience, I am developing the Oxidefier tool to automatically translate Solidity smart contracts to Rust, so I have deep knowledge of how a translation can be done. At Formal Land, we are very experienced in formal verification, and we developed the tools coq-of-solidty and coq-of-rust, which we would use to prove the equivalence.

We are familiar with zero-knowledge technology, developing a formal verification framework for circuits named Garden.

Start date

We can start on June 15th.