ProofForge

davirain-su/proof_forge

**ProofForge** is an early-stage but architecturally ambitious **Lean-first multi-chain smart-contract platform**. It aims to let developers write a single verified contract in Lean (with formal anchors) that compiles, tests, and deploys across heterogeneous blockchains while preserving semantics and catching incompatibilities at compile time. ### Core Idea The central thesis (quoted directly from the README): > “ProofForge’s goal is one verified Lean contract codebase that can be compiled, tested, and deployed across multiple blockchain target families. Contracts are written against a chain-neutral Contract Intent API; the compiler lowers them to a portable IR, routes capabilities per target, and emits chain-native artifacts. Unsupported target capabilities are rejected at compile time instead of silently changing semantics.” Instead of the usual “write once, debug everywhere” or per-chain rewrites, ProofForge introduces a **portable IR** as the semantic anchor. A **capability registry** + **target routing** layer decides what a given chain can actually support and rejects anything that would change observable behavior. Chain-specific features (e.g., Solana PDA/CPI) live in gated **Target Extension SDKs** rather than polluting the portable core. This creates a single source of truth in Lean for business logic, state machines, invariants, and proofs, while still producing native artifacts (EVM bytecode, Solana sBPF ELF, NEAR Wasm, Sui Move, etc.). ### Traction **Very early / pre-visibility stage**: - **Stars**: 1 - **Forks**: 1 - **Watchers**: 0 - No published releases or public packages **High internal velocity and engineering discipline**: - ~1,579 commits on `main` - Extremely active development (commits and PRs as recently as yesterday, July 12, 2026) - Recent focus: hardening the “primary triad” (EVM + Solana sBPF + NEAR Wasm), runtime safety, ValueVault scenarios, and post-consolidation cleanup after the July 2026 branch work - **P0 backend-gate covenant (D-045)** is now closed for the three primary