Quickstart

Install the toolchain and compile your first ProofForge contract to EVM bytecode

Prerequisites

Install these tools first:

• elan — Lean toolchain manager (uses the repo-pinned lean-toolchain).
• just — command runner, from casey/just.
• solc (0.8.30) and Foundry (forge/cast/anvil) — only needed for the EVM target.

Build

git clone https://github.com/DaviRain-Su/proof_forge.git
cd proof_forge
elan toolchain install "$(cat lean-toolchain)"
lake build

The root justfile is the developer-facing command catalog and CI entrypoint:

just --list        # list all recipes
just build         # lake build
just check         # fast static gates (Lean + EVM + Psy)
just evm-all       # full EVM gates: examples, Foundry smoke, Anvil deploy
just ci            # the full CI sequence locally

Compile a contract

Compile the EVM Counter example to runtime bytecode:

lake env proof-forge --evm-bytecode --root . --module contract \
  -o build/evm/Counter.bin Examples/Evm/Contracts/Counter.lean

Emit artifacts for other targets from built-in portable IR fixtures:

lake env proof-forge --emit-counter-emitwat -o build/wasm-near   # NEAR Wasm
lake env proof-forge --solana-elf -o build/solana/counter.so     # Solana ELF
lake env proof-forge --emit-counter-ir-psy -o build/psy/Counter.psy
lake env proof-forge --emit-counter-ir-leo -o build/aleo         # Aleo Leo
lake env proof-forge --emit-counter-ir-ts -o build/ts/Counter.ts # CF Workers

Lean commands must run through lake env ... so the toolchain environment is set correctly.

Next steps

Onboarding

Full local setup, editor config, and the minimum validation loop.

Architecture

How the compiler lowers Lean sources to chain-native artifacts.

Backend status

Which targets are mature, experimental, or research.

Validation gates

The runnable gates and tool prerequisites for every target.