# formal-land/rocq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

Repository: https://github.com/formal-land/rocq-of-rust
Canonical: https://ross.abutalabs.com/products/rocq-of-rust
Homepage: https://formal.land/docs/tools/rocq-of-rust/introduction
Language: Rocq Prover
License Family: other
Topics: formal-verification, rust, proof, rocq
Last push: 2026-09-02T11:45:03+00:00

## Health v2 (maintenance only)
Score: 76/100 (v2, computed 2026-09-03T02:20:16.233290+00:00)
- activity 100, release rhythm 35, longevity 96
- inputs: {"age_days": 1344, "days_push": 0, "days_rel": null, "gap_med": null, "n_releases_24m": 0}
- flags: no_releases, no_license
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 1161, forks 44 (observed 2026-09-03T02:15:12.054467+00:00)

## What it is
rocq-of-rust is a formal verification tool that translates Rust programs (from the compiler's THIR representation) into the Rocq proof assistant so that correctness and security properties can be mathematically proven for all inputs. It is developed by Formal Land, funded by the Ethereum Foundation and Aleph Zero Foundation, and is a work in progress.

## Use cases
- formally verify a Rust program for all possible inputs
- prove absence of panics and security vulnerabilities in Rust code
- translate Rust code to Rocq for interactive theorem proving
- verify a Rust implementation of the Ethereum virtual machine
- reusable machine-checked proofs that re-run as code evolves
- audit critical Rust libraries beyond what testing can cover

## When to choose
- you need mathematical guarantees for critical Rust code, such as blockchain infrastructure or security-sensitive libraries
- you want proofs that can be replayed and maintained as the codebase changes
- you are verifying Rust implementations of virtual machines or cryptographic primitives

## When to avoid
- you just want quick bug-finding with fuzzing or static analysis rather than full proofs
- your codebase is large and you cannot invest in writing specifications and Rocq proofs
- you need a fully automated, turnkey verification tool - the tool is a work in progress and requires manual linking and simulation steps

## Facets
- artifact type: cli-tool
- maturity: active
- function: compiler, security, testing, developer-tools
- domain: security, programming-languages, blockchain, developer-tools
- platform: rust, cli
- tags: formal-verification, theorem-proving, rocq, coq, rust-analysis, proof-assistant, thir, smart-contracts, evm, algorithms, linux, macos

## Member repositories
- formal-land/rocq-of-rust (main) score 76

## Provenance
- Observed fields: from GitHub, fetched 2026-09-03T02:15:12.054467+00:00.
- Health v2: computed from the inputs above; adoption is never an input.
- Inferred fields (summary, facets, guidance): AI-extracted, prompt v1, taxonomy v1, on 2026-08-30T06:31:53.759476+00:00, confidence not recorded.
  - readme: https://github.com/formal-land/rocq-of-rust (fetched 2026-09-03T02:15:12.054467+00:00, sha 24da49fbf9de)
  - homepage: https://formal.land/docs/tools/rocq-of-rust/introduction (fetched 2026-08-29T12:36:36.443258+00:00, sha 1da88839e1d3)
  - site_page: https://formal.land/docs/audit (fetched 2026-08-29T12:36:36.445951+00:00, sha e51886c83c3c)
  - site_page: https://formal.land/docs/tools (fetched 2026-08-29T12:36:36.447735+00:00, sha eddc5d879e86)
  - site_page: https://formal.land/docs/company/about (fetched 2026-08-29T12:36:36.449398+00:00, sha 5e6a1b65c152)
  - site_page: https://formal.land/docs/learn/start (fetched 2026-08-29T12:36:36.451324+00:00, sha 52ba998f5904)
  - site_page: https://formal.land/docs/tools/rocq-of-rust/revm-project (fetched 2026-08-29T12:36:36.453159+00:00, sha bd0caa8114e4)
  - site_page: https://formal.land/docs/tools/rocq-of-rust/links (fetched 2026-08-29T12:36:36.454901+00:00, sha f8d6c7efd3dd)
  - site_page: https://formal.land/docs/tools/rocq-of-solidity/introduction (fetched 2026-08-29T12:36:36.456951+00:00, sha 7182c10465b1)
  - site_page: https://formal.land/docs/tools/garden/introduction (fetched 2026-08-29T12:36:36.458784+00:00, sha 19c818fa715e)
- Data as of 2026-08-30T08:39:29.467469+00:00.