rocq-of-rust: proving a Rust program correct, one translation at a time

The point is not fewer bugs, it is a different kind of claim

The README opens with an argument that is worth taking seriously. Even if the type system of Rust prevents many mistakes, including memory errors, the code is still not immune to vulnerabilities such as security vulnerabilities, unexpected panics, or wrongly implemented business rules.

That is the gap rocq-of-rust aims at. The proposed answer is to mathematically prove that the code implements its specification for all inputs, which is what the project calls formal verification. The README is careful to say the tool is a work in progress in many parts, and that although it aims to provide better coverage than testing or manual reviewing, the best route to a 100 percent guarantee is to additionally lower the verification down to the assembly level.

That caveat is the most important sentence in the document. A proof about a translated program is a proof about the translation, and the gap between the translation and the machine code is exactly where the remaining uncertainty lives. Stating it plainly is a good sign about the project.

The commercial context is also stated. The project offers formal verification as a service, including designing the specification and the proofs, and the README says the work was mainly funded by the Ethereum Foundation and the Aleph Zero Foundation.

THIR, linking and simulation, in that order

At the heart of the tool is the translation of Rust programs to idiomatic code in the Rocq theorem prover. Once the code is in Rocq it can be verified with standard proof techniques, which is the whole architecture in one sentence.

The translation happens in three steps, and the naming is what makes the approach readable. First, the THIR representation of Rust is imported into Rocq by running cargo rocq-of-rust. Second, type checking and trait inference are performed with native Rocq types and typeclasses, which the project calls linking. Third, the control flow and memory manipulations are represented in a purely functional style, which the project calls simulation.

The example makes the shape concrete. A Rust function:

fn add_one(x: u32) -> u32 {
    x + 1
}

is proved equivalent to a purely functional Rocq definition:

Definition add_one (x : u32) : u32 :=
  x +i 1.

The Rocq form is not a transliteration. It uses a machine integer notation, and the THIR representation in Rocq for the same function is a monadic computation over a list of values and types, allocating the argument and calling a closure with a wrapped addition and a literal one, with an impossible case for the wrong number of arguments. That verbosity is the point of the three stages: the automatic translation is deliberately noisy, and the two semi-automated refinement steps gradually make it amenable to proof.

The repository's own examples directory shows the range of work, with folders for a custom case, ink contracts, a monadic transformation and the Rust book, plus a file called subtle.rs that suggests the interesting cases live in the corner cases.

Specifications are the actual deliverable

The workflow described in the README is: generate an automatic translation of the Rust to Rocq, go through the linking and simulation refinement steps, then write the specifications and prove that the program fulfils them for any possible user input.

The examples of specifications given are the most useful part of the document, because they show what a formal specification is in practice. The code cannot panic. This clever data structure is equivalent to its naive version, except for the execution time. This new release, which introduces new endpoints and does a lot of refactoring, is fully backward-compatible with the previous version. Data invariants are properly preserved. The storage system is sound, as what goes in goes out, which the README says generally amounts to stating that the serialization and deserialization functions are inverse. The implementation behaves as a special case of what the whitepaper describes once formally expressed.

Read together, these are a set of properties that are usually asserted in review and never checked. A backward-compatibility guarantee, a storage round-trip, a data structure equivalence, a panic freedom proof. Each of those is a research project in its own right, and each of them is checkable, which is the argument the tool is making.

The specifications and the proofs are written in Rocq, in a file the workflow calls proofs, and the guarantee produced is stated as a program that is 100 percent reliable, which is the project's word for it and also the word a reviewer should treat with care.

Revm is the test case, and it is funded

The project points at one substantial application: it is currently verifying Revm, a Rust implementation of the Ethereum virtual machine, to show it equivalent to a specification written in a purely functional style. The work is ongoing, in the folder RocqOfRust/revm, and it is funded by a grant from the Ethereum Foundation.

That choice of target is informative in several ways. The EVM implementation is code whose correctness has direct economic consequences, it is a large program written in exactly the language rocq-of-rust handles, and the specification it is compared against, a purely functional model of the EVM, is the sort of thing that already exists in a different formalisation tradition. The verification therefore doubles as a demonstration that the translation scales past a toy.

It is also a statement about the intended user. The people funding and building this are working on consensus-adjacent and cryptographic code, where the argument that a proof is worth more than a test suite is a practical one rather than an academic one.

For a newcomer, the Revm work is the best documentation available, since it shows the specifications that get written for real code and the shape the proofs take when the program is not a three-line function.

The alternatives, and how each one starts from a different place

The README lists the other projects working on formal verification for Rust, and the differences are precise enough to be useful.

Aeneas translates from MIR to purely functional Rocq or F* code and puts the code automatically into a functional form. Hax translates from THIR to Rocq, F* or Lean code. Creusot translates from MIR to Why3, and then to SMT solvers. Verus does automatic verification for Rust with annotations. Kani does model checking with CBMC.

So the axes are the starting point, the target, and the method. rocq-of-rust starts from THIR like Hax does, but aims at Rocq with a manual refinement step rather than an automatic functionalisation, and it uses a proof assistant with manual proofs rather than an SMT solver or a model checker. Aeneas and Creusot start one step earlier, from MIR, which is closer to the compiler's own intermediate form.

The practical consequence is effort. An SMT-backed or model-checking approach aims to discharge the proof automatically, which is faster and less complete. A proof-assistant approach asks a human to write the specification and the proof, which is slower and total. For code where the specification itself is the interesting artefact, that trade is usually worth making.

The README also notes that a bit of code in this project was taken from Creusot, to make the Cargo command rocq-of-rust run the translation in the same context as Cargo, which is a fair example of how closely these projects overlap.

Dual licensing, and the split between proofs and transpiler

The licensing is stated as dual, and the split follows the directory structure. The Rocq proofs and libraries under RocqOfRust/ are MIT licensed, and the Rust transpiler under cli/ and lib/ is AGPL-3.0 licensed, with a LICENSE file in each of those places.

The AGPL component is the one to think about. It is a strong copyleft licence, and for a tool that a company would run against its own codebase, the question of whether running the tool creates obligations is exactly the kind of question that needs an answer before, not after, adoption. The MIT side, covering the proofs and the Rocq libraries, is permissive and can be reused in a proprietary verification effort.

The repository layout shows how the two halves meet. The Cargo workspace has members lib and cli, with the ink integration tests for an ERC20 excluded, and the tree also contains contracts/, docs/, examples/, an ink/ directory, third-party/ for vendored code, run_tests.py, a rust-toolchain file, a clippy.toml and an AGENT.md.

The documentation is split in the same spirit, with a build tutorial in docs/BUILD.md and a user guide in docs/GUIDE.md that introduces the command line interface and lists the supported options. The prerequisites are short: Rust and Rocq, with the Rocq package definition given in RocqOfRust/rocq-of-rust.opam.

Where rocq-of-rust is the wrong tool today

The first wrong-tool case is a team that wants a fast safety net. The workflow the README describes, translate, refine with linking and simulation, write specifications, write proofs, is a programme of work measured in months, not a step in a pull request. A project that wants continuous assurance on every commit is better served by property tests, fuzzing or a model checker, and the README's own list includes Kani, which uses CBMC, precisely for that kind of automated checking.

The second is code whose specification is not written down. The tool's value depends entirely on there being a specification to prove against, and in most organisations the specification of a service is a set of tests and a wiki page. The first real task is not proving anything but deciding what the properties are, and that is a product conversation rather than a technical one.

The third is a project that needs the machine code covered. The README says the best route to a 100 percent guarantee is to additionally lower the verification to the assembly level, and that step is not what this tool does. A team with a threat model that includes a compiler or a hardware assumption is still relying on trust that this project does not remove.

There is also the maturity point, made plainly in the README itself, that the tool is a work in progress in many parts. For a project with a support commitment, the option the project offers is a verification service with the specifications and proofs designed for them, and that is a different kind of engagement from running the tool in your own pipeline.

Editorial conclusion

Adopt rocq-of-rust if you are working on a critical Rust codebase, a smart contract or a database engine, and you can budget for the kind of work formal methods demand, which is writing specifications before writing proofs. Do not adopt it as a lint or a test substitute, since it is a research-grade translation whose own README calls it a work in progress, and do not expect a one-command guarantee, because the README also says that for a full guarantee you would want to lower the verification to the assembly level. Before you commit, read docs/BUILD.md and docs/GUIDE.md, check the dual licensing, since the Rust transpiler is AGPL-3.0 while the Rocq libraries are MIT, and decide whether the service offering that the project describes is a better fit than running the tool yourself.

Frequently asked questions

Official sources

1. formal-land/rocq-of-rust on GitHub
2. Issues
3. Project website
4. README