Introduction
ProofForge V2
A Lean 4 multi-target compiler. Authors write one portable program; the compiler infers semantic requirements and materializes verifiably per target.
This site is a portal. Authoritative specifications, ADRs and implementation logs live in the repository under /docs. Each page here links back to the source of truth on GitHub.
How to read
- Getting started — install Lean, build, run the Counter example.
- Architecture — layers, modules, forbidden dependencies.
- Compilation pipeline — Parse → Typed → Semantic → Resolve → Materialize.
- Targets — EVM · Solana · NEAR · Noir, with honest maturity.
- Invariants — what the compiler will not do.
- CLI & CI — just commands and clean-room gate.
Status
V2 has established the documentation and specification baseline plus a not-releasable alpha skeleton: independent Lake project, unified DSL entry, and the minimum connectivity through Core and the four target materializers. This is not equivalent to Phase 1 being complete.
Read the full doc index on GitHub →