merc-verified

Formal verification of labelled transition system (LTS) algorithms. Rust implementations in crate/ are translated to Lean 4 via Aeneas and verified against formal definitions in MercVerified/.

We want to prove the correctness of the merc repository. For this we introduce a derived crate of (simplified) Rust code that we can translate to Lean and verify. The MercVerified/ directory contains the formal definitions and proofs, while Code contains the generated Lean code from the Rust implementations.

Documentation

The API documentation, generated by doc-gen4, is published to GitHub Pages at https://mercorg.github.io/merc-verified/ on every push to main.

To build it locally, use the separate docbuild package (so that doc-gen4 is not a dependency of the project itself):

cd docbuild
MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4
lake build MercVerified:docs MercLib:docs

The first build also documents all of Mathlib and takes a long time. Open docbuild/.lake/build/doc/index.html to view the result; a static file server (e.g. python3 -m http.server -d .lake/build/doc) is needed for the search to work.

Prerequisites

• Rust (stable toolchain)
• Lean 4 (managed via elan)
• OCaml 5.3 (via opam, for building Aeneas)

Getting Started

1. Initialize the submodules

Use the following command to initialize the git submodule:

git submodule update --init --recursive

2. Build Charon and Aeneas

Charon compiles Rust to LLBC, and Aeneas translates LLBC to Lean.

# Install OCaml dependencies
opam switch create 5.3.0

opam install ppx_deriving ppx_deriving_yojson visitors easy_logging zarith yojson core_unix odoc \
  ocamlgraph menhir ocamlformat.0.27.0 unionFind zarith progress domainslib

cd 3rd-party/aeneas

# Build Charon (Rust → LLBC compiler)
eval $(opam env)
make setup-charon

# Build Aeneas (LLBC → Lean translator)
make
cd ..

3. Generate Lean code from Rust

# Generate LLBC from the Rust crate
cd verified
../3rd-party/aeneas/charon/bin/charon cargo --preset=aeneas
cd ..

# Translate LLBC to Lean
./3rd-party/aeneas/bin/aeneas -split-files -backend=lean -dest=. -subdir=MercVerified/Code ./verified/verified.llbc

# Strip absolute paths from generated `Source:` comments, so regenerating on
# a different machine/checkout doesn't produce a spurious diff
python3 scripts/strip_source_paths.py

The generated Lean files will appear in MercVerified/Code/.

4. Build the Lean project

lake build

This builds both the formal definitions in MercVerified/ and the generated code in MercVerified/Code/, checking all proofs.

5. Proving with AI agents

Install the uv Python package manager for the lean-lsp-mcp. A MCP is a Model Context Protocol that allows AI agents to connect to external programs, in this case interacting with lean.

cargo install uv