Skip to main content

​
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.