Lusterna by Certora
Experimental

Agents write the proofs.
Lean checks every one.

AI agents can translate Rust to Lean 4 and prove properties about it. But an agent will also report a theorem as proved when its proof rests on a sorry, an unproven axiom, or a weakened statement. Lusterna lets agents do this work on Rust and Solana programs and checks every result itself: the Lean kernel checks each proof, and the harness rejects any proof that rests on an unproven assumption.

Get started View on GitHub

How it works

You provide a Rust repository and a short note on what to focus on. Lusterna runs five stages on it, each a separate agent, and checks each stage's output before the next one starts.

  1. 01

    Infer

    Choose the functions to verify and describe their intended behavior.

  2. 02

    Translate

    Translate those functions to Lean 4 with Charon and Aeneas.

  3. 03

    Formalise

    State the intended behavior as Lean theorems.

  4. 04

    Prove

    Prove the theorems, or refute false ones with a counterexample.

  5. 05

    Report

    Write a report that opens with the harness's list of proved theorems.

Get started

You need Python 3.10+, Docker, and an Anthropic API key. Point Lusterna at a git repository, and it adds the results to that repository as a new branch.

shell
git clone https://github.com/Certora/lusterna && cd lusterna
python3 -m venv .venv && source .venv/bin/activate
pip install -e .

lusterna build-image                      # one time
export ANTHROPIC_API_KEY=sk-...
lusterna run /path/to/rust-repo design.md

Usage Pipeline Design