ProofForge is a Lean 4 compiler profile for Solana and EVM smart contracts. Write the contract as an ordinary def. Prove it as an ordinary theorem. Compile the same subject to on-chain bytes.
It is not a new contract language. There is no program … where. Mark callable roots with @[pf_entry]. The CLI is pf.
Current targets: Solana sBPF (.so / IDL), EVM Yul (.bin / ABI),
XRPL Bedrock WASM, and NEAR Protocol WASM (.wat / .wasm).
- Website: https://davirain-su.github.io/ProofForge/
- Docs index: docs/INDEX.md
Lean 4 is already an executable language and a proof assistant. ProofForge only adds the on-chain profile:
| Principle | What it means |
|---|---|
| One subject | Theorems pin the user def. Compile walks the same extracted IR. You never prove A and emit B. |
| Fail-closed subset | Profile admits only what can lower on-chain. IO, partial, sorry, @[extern], @[implemented_by], and unbounded recursion are refusals, not warnings. |
| Two profiles, one Core | SVM and EVM share Lean / Profile / Extract / CFG. They do not share a physical store. |
| Honest trust boundary | The kernel accepts theorems about the def / IR. That is not a claim about the loader or mainnet. |
ordinary Lean def / theorem ← Lean owns this
│
▼
Profile (fail-closed subset)
│
▼
Extract Expr → typed Core + target-neutral Ops
│
┌───┴───┐
▼ ▼
SVM IR EVM IR
+ IDL + ABI
│ │
▼ ▼
sBPF / .so Yul / .bin
#pf_build Examples.Counter extracts inside Lean. pf build --target svm walks the same IR.
Do not substitute a random assembler from PATH. Install the locked versions with:
./.agents/setup| Tool | Version | Role |
|---|---|---|
| Lean 4 | v4.31.0 |
Source language and kernel |
| sbpf | 0.2.2 |
Assemble .s → Solana .so |
| solc | 0.8.34 |
Assemble Yul → EVM .bin |
| Surfpool | 1.5.0 |
Loader-v3 local deploy (not solana-test-validator) |
| Foundry / Anvil | 1.7.1 |
EVM engineering gate |
| Rust | 1.90.0 |
Mollusk runtime tests |
lake buildThis type-checks ProofForge, the examples, and produces the pf executable. It does not emit on-chain artifacts.
pf re-extracts IR from the user module. It does not assemble a legacy Golden fixture.
# Solana: Counter.so / Counter.s / Counter.idl.json
lake exe pf -- build --target svm --out build/sbpf Counter
# EVM: Counter.bin / Counter.yul / Counter.abi.json
lake exe pf -- build --target evm --out build/evm Counter
# WASM family members
lake exe pf -- build --target xrpl --out build/xrpl Counter
lake exe pf -- build --target near --out build/near Counter--target svm also accepts solana or sbpf. Omit the program name to build every registered module for that target. See lake exe pf -- --help.
WASM is a chain family: each chain owns its host imports and storage layout. XRPL uses its
Bedrock/XLS-0102 boundaries; NEAR uses chain-owned env imports and a fail-closed bounded ABI.
See docs/modules/xrpl.md and docs/modules/near.md.
Neither target name is a blanket public-deployment or standard-ABI compatibility claim.
| Target | Artifacts | Layout |
|---|---|---|
| SVM | .so / .s / .idl.json |
Solana IDL spec 0.1.0, Loader V3 |
| EVM | .bin / .yul / .abi.json |
Selector / storage slots / ABI |
| XRPL | .wat / .wasm |
Chain-owned Bedrock/XLS-0102 host boundaries |
| NEAR | .wat / .wasm |
env imports, bounded chain-owned ABI |
Contracts should import a target SDK, not the ProofForge umbrella (that pulls Emit / Assemble / Registry).
| Target | Import |
|---|---|
| Solana / sBPF | ProofForge.Attr + ProofForge.Svm.Sdk |
| EVM | ProofForge.Attr + ProofForge.Evm.Sdk |
Good in-tree examples: Examples/Svm/VersionedLedger.lean (SVM), Examples/Evm/TipJar.lean (EVM). Minimal shape:
import ProofForge.Attr
import ProofForge.Svm.Sdk
namespace MyProgram.Counter
structure State where
value : UInt64
inductive Error where
| overflow
@[pf_entry]
def init (initial : UInt64) : State :=
{ value := initial }
@[pf_entry]
def increment (s : State) (delta : UInt64) :
Except Error (State × UInt64) :=
if s.value ≤ u64Max - delta then
let next := s.value + delta
.ok ({ value := next }, next)
else
.error .overflowInline helpers with @[pf_inline]. Lean still owns business typing. Extract authority is the elaborated Expr closure, not Lean.Compiler.IR.
Theorems live in the same file, in a Proofs section. They are ordinary kernel-checked properties of the @[pf_entry] functions.
First batch (Counter, Capped, Token):
- success-path postconditions
- monotonicity
- Token supply effect
- Capped cap invariant
They depend only on the standard axioms propext / Quot.sound. CI (scripts/check_no_sorry.py) refuses placeholders in the proof batch. Proof subject and compile subject must share the same IR digest.
These are not part of lake build. Run them after pf has written artifacts.
Environment variables use the PF_*_SO prefix:
(cd runtime-tests/solana && \
PF_COUNTER_SO=../../build/sbpf/Counter.so \
cargo test --locked --test counter)Phoenix and the Phoenix-v1 profile verifier deploy through Surfpool, not solana-test-validator:
runtime-tests/surfpool/smoke.sh
runtime-tests/surfpool/smoke.sh PhoenixV1ProfileEVM engineering gate is pinned Anvil. v0 refuses public broadcast.
SVM owns account geometry, CPI, and IDL. Persistent maps and queues are fixed-capacity POD views on account bytes. Heap is an invocation-local downward bump (32 KiB, up to 256 KiB): dealloc does not reclaim, and pointers never enter accounts.
Compiler boundary:
Svm.EntryAdapterowns packed wire decode, raw/generated dispatch, and the account prefix.Svm.AccountStorageowns in-account Region/Field and boundedQuery/Call(map, queue, allocator, tree).- Generic Ops / IR / CFG / main Emit dispatch
componentonce. New containers extend a component-owned module; they do not cut sideways through Extract or the main emitter.
Examples/Svm/PhoenixV1Profile.lean is the current stress test of that boundary — not a special-case compiler.
| Area | What is in tree |
|---|---|
| Storage | 128-seat trader tree and two 512-node order books live in account bytes. Slots are one-based (0 is sentinel). No heap Map, detached node, copied tree, or out-of-account pointer. |
| Matching | Fixed-capacity Sokoban insert/remove, trader get-or-register deposit, bid/ask ReduceOrderWithFreeFunds (partial and full), collateral unlock, checked preflight. |
| Official tags 3–14 | Tag 3 PlaceLimit (strict subset: PostOnly, no TIF, deposited funds only). Tags 4/5 ReduceOrder(WithFreeFunds) partial and full. Tags 6/7 FifoCancel cancel in place (bids→asks, per-side FIFO) with owner filter, unlock, event index, and released-lot accumulator; tag 6 then claims/withdraws quote→base, tag 7 never enters Token CPI. Tags 8/9 CancelUpTo add side + optional tick/search/cancel caps over a bounded FIFO filter. Tags 10/11 CancelMultipleOrdersById (bounded id vectors). Tag 12 WithdrawFunds, tag 13 DepositFunds (Option<u64> all-variant), tag 14 RequestSeat (System CPI seat PDA + trader register). |
| Audit | BatchRecorder.begin/append/finish uses the official SDK 0x300000000 / 32 KiB downward bump. 32 × 35-byte Reduce records flush before the 33rd. Empty finish still emits a 93-byte header-only batch. Heap addresses do not enter source or accounts. |
| Cursors | PDA mint seeds read an authenticated MarketHeader byte slice. FIFO cursors keep a (price, sequence) scalar key and walk a bounded strict upper-bound from the account root. Deletes do not store node addresses or collect a heap Vec. |
The official wire surface currently lands tags 3–14 on the same component boundary. Details: docs/modules/phoenix.md.
EVM shares ordinary Lean, Profile, Extract, and Core CFG with SVM. It does not copy SVM account geometry.
Contract source opens ProofForge.Evm.Sdk:
Storage.Layoutis a compile-time cursor for typed hashed mapsAddress,UInt256,Context,Immutable,Event,Revert- closed-call facade — it does not hide
.ok/.error
Descriptors erase at extract time and never enter storage. Examples.Evm.Token and Examples.Evm.Capped already sit on this surface with an unchanged target IR digest.
| Claim | Meaning |
|---|---|
| Weak (public v0) | The kernel accepted theorems about the user def / extracted IR. TCB = Lean kernel + subject binding. |
| Engineering | The same IR, through the emitter and pinned sbpf / solc, matches fixtures on Mollusk or Anvil. |
| Not claimed | .so / loader / full SVM refinement / theorem ⇒ deployed program. A theorem does not imply a correct public deployment. |
On-chain discriminators and layout still use the proof-forge-solana-v1: domain. Renaming this repository does not change chain bytes.
The product site lives in website/ — same repository, not a second project. GitHub Pages: https://davirain-su.github.io/ProofForge/.
cd website && npm install && npm run devAfter the first merge, set Settings → Pages → Source to GitHub Actions.
Remote MCP serves docs and scaffold guidance only. It does not spawn Lean, hold keys, or broadcast:
https://proof-forge-mcp.davirain-yin.workers.dev/mcp
proof_forge is the earlier program … where DSL. This repository reuses Lean syntax itself and extracts the fail-closed subset that can lower on-chain.
The first kernel-checked contract properties live in each example's Proofs section
(Examples/Counter.lean, Examples/Capped.lean, Examples/Token.lean): exact success
postconditions, monotonicity, Token supply effects, and the Capped cap invariant, all on
standard axioms propext / Quot.sound only. The sBPF L3 bridge in
ProofForge/Svm/Solanalib.lean additionally uses native_decide (Lean.ofReduceBool)
for its concrete checks, so its trust base is wider.
Before opening or merging a PR, reproduce the Lean / SVM lane gates locally:
python3 scripts/check_ownership.py
python3 scripts/check_no_sorry.py
lake build
lake build Tests.ProofSpec Tests.SolanalibSpec Tests.SemanticsSpec
lake build Testscheck_ownership.py: blocksExamples→Emitimports and Runtime/SDK protocol-word leaks; failures printpath:line: ….check_no_sorry.py: scansProofForge/,Examples/,Tests/forsorry/sorryAx; whitelist is negative fixtures only (see script header); failures printrel:line: message.Tests.ProofSpec/SolanalibSpec/SemanticsSpec: named Track A and L3-bridge goals; CI's Lean lane pins these before fulllake build Tests. The SVM lane also runs ownership + no-sorry, then builds/runs Mollusk.
Start at docs/INDEX.md.
| Doc | Role |
|---|---|
| 01-prd.md | In / out of scope |
| 02-architecture.md | Module and trust boundaries |
| modules/README.md | Per-module contracts |
| plan/svm-work-plan.md | Current SVM mainline |