Pinned Loading

1. ProofForge ProofForge Public

   Lean 4 compiler profile: ordinary Lean defs to Solana sBPF and EVM Yul. Not a new contract language.

   Lean 1

2. ProofForgeEvm ProofForgeEvm Public

   Lean 4 → EVM compiler: mark contract entries with @[pf_entry], extract a checked IR from Lean sources, emit Yul, assemble to EVM bytecode via solc. EVM-only fork of ProofForge.

   Lean

3. ProofForgeSvm ProofForgeSvm Public

   ProofForge SVM: Lean 4 → Solana sBPF program compiler (SVM single-target fork of ProofForge)

   Lean

4. ProofForgeNear ProofForgeNear Public

   Lean 4 → NEAR Wasm compiler: mark contract entries with @[pf_entry], extract a checked IR from Lean sources, emit WAT, assemble to .wasm via pinned wat2wasm. near-sdk-style SDK (storage, NEP-141, p…

   Lean

5. ProofForgePsy ProofForgePsy Public

   Lean 4 → PSY (DPN circuit) contract compiler — Psy single-target fork of ProofForge (psy-dpn-v1)

   Lean

6. ProofForgeCommon ProofForgeCommon Public

   Shared ProofForge surface (Attr, Core, Crypto, Profile) for the ProofForgeEvm/Svm/Near/Psy target compilers

   Lean