Getting started

1. Toolchain

The pinned Lean toolchain is declared in the repository's lean-toolchain file. Install elan first, then Lean will be provisioned automatically on first build.

curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
git clone https://github.com/DaviRain-Su/proof_forge
cd proof_forge

2. Build and test

just build     # Lake: ProofForgeV2 + proof-forge-next
just test      # proof-forge-next-tests
just ci        # portable Linux / GitHub CI subset

3. Your first program

The Counter is the canonical portable program:

import ProofForgeV2
open ProofForgeV2.Language

program Counter where
  state count : UInt64

  init(initial : UInt64) do
    count := initial

  entry increment(delta : UInt64) : UInt64 do
    count := count + delta
    return count

  view get() : UInt64 do
    return count

4. Choose a target

Targets are selected on the compiler command line, never in the source. The source never mentions “contract”, “circuit” or “zkVM workload” categories.

proof-forge-next build --target evm      # or solana / near / noir

Full quickstart on GitHub →