Skip to main content

🦀 coq-of-rust

note

This project was funded by the Aleph Zero Foundation.

Our Rust analyzer coq-of-rust provides:

  • The highest level of security 🛡️ for your Rust programs by checking all possible user inputs 🔍 (formal verification).
  • A verification of any kinds of security properties 👮 (interactive prover).
  • Reusable proofs 🔁 you can re-run as the code evolves, eliminating the need of costly manual code audits.

This is better than testing that might miss some edge cases. In fact, we always find all the bugs!1

Service

We apply coq-of-rust to formally verify your Rust programs, writing the specifications and proofs of correctness. See our project for Sui as a reference.

This is the highest level of security 💫 and this is accessible now, so it would be a big miss not to use it. This is the only way to ensure full protection of your code even against state-level attackers 🦸, as much as encryption fully protects your data.

The cost is only $10 💵 per line of Rust code! 🥹

🦸 Get started!    $10/loc

We always verify the first 100 lines for free 🎁. We have a limited availability for now, so be quick! 🏇

How it works​

It converts Rust programs to the 🐓 Coq proof system. You access the source on GitHub. coq-of-rust generates a shallow embedding of Rust into Coq. We run the translation from the THIR level of the Rust compiler. The generated Coq code is more verbose than the source Rust as we explicit all the low-level details, such as the sequencing of effects or the implicit borrowing/dereferencing.

Example​

coq-of-rust translates the Rust code:

fn balance_of(&self, owner: AccountId) -> Balance {
    self.balance_of_impl(&owner)
}

to the Coq code:

(* Generated by coq-of-rust *)
Definition balance_of
    (self : ref ltac:(Self))
    (owner : erc20.AccountId.t)
    : M ltac:(erc20.Balance) :=
  let* self : M.Val (ref ltac:(Self)) := M.alloc self in
  let* owner : M.Val erc20.AccountId.t := M.alloc owner in
  let* α0 : ref erc20.Erc20.t := M.read self in
  erc20.Erc20.t::["balance_of_impl"] α0 (borrow owner).

Workflow​

To formally verify a Rust project using coq-of-rust we work as follows:

  1. translate the Rust code to Coq using coq-of-rust
  2. define the memory of the program (how the values will be allocated)
  3. write simulation functions for each function of the Rust code, to give a simpler and more functional definition of the code
  4. verify that these simulations are equivalent to the source code
  5. prove properties over these simulations

As some of the work is very verbose and repetitive, such as the definition of the simulation functions, but thankfully generative AI tools such as Github Copilot are better and better at code generation.

Footnotes​

  1. What does this mean? We assume given a formal specification of the code that mathematically describes what is supposed to be a bug and what is supposed to be a feature. From the there, the Coq proof system that we use can check that the code is correct with respect to this specification for all possible user inputs. The result is a mathematical proof checked by the computer. Almost any programs can be verified except the proof checker itself, as it would be a paradox. See this paper to see how Coq was used to make the only C compiler without bugs (well, except on the non formally verified parts). ↩