> ## Documentation Index
> Fetch the complete documentation index at: https://gradiences.mintlify.site/llms.txt
> Use this file to discover all available pages before exploring further.

# 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](https://github.com/casey/just).
* **`solc`** (0.8.30) and **Foundry** (`forge`/`cast`/`anvil`) — only needed for
  the EVM target.

## Build

```sh theme={null}
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:

```sh theme={null}
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:

```sh theme={null}
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:

```sh theme={null}
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
```

<Tip>
  Lean commands must run through `lake env ...` so the toolchain environment is
  set correctly.
</Tip>

## Next steps

<CardGroup cols={2}>
  <Card title="Onboarding" icon="door-open" href="/onboarding">
    Full local setup, editor config, and the minimum validation loop.
  </Card>

  <Card title="Architecture" icon="sitemap" href="/architecture">
    How the compiler lowers Lean sources to chain-native artifacts.
  </Card>

  <Card title="Backend status" icon="circle-check" href="/backend-status">
    Which targets are mature, experimental, or research.
  </Card>

  <Card title="Validation gates" icon="shield-halved" href="/reference/validation-gates">
    The runnable gates and tool prerequisites for every target.
  </Card>
</CardGroup>