One portable program. Many verifiable targets.
ProofForge V2 is a Lean 4 multi-target compiler. Authors write one program; the compiler infers semantic requirements, then --target selects materialization for EVM, Solana, NEAR and Noir. Changing target must not change meaning.
The whole program.
No target keywords, no chain-specific syntax. State, init, entry, view — same source compiles to bytecode, sBPF plan, Wasm, or a Noir circuit.
import ProofForgeV2
open ProofForgeV2.Language
program Counter where
state count : UInt64
init(initial : UInt64) do
count := initial
entry increment(delta : UInt64) : UInt64 do
count := count + delta
return count
view get() : UInt64 do
return countMaterialize honestly.
Parse → Typed → Semantic → Resolve → Materialize
Any failure fails closed. No best-effort downgrade, no legacy fallback path. Source, Typed and Semantic layers never branch on TargetId.
EVM
Counter bytecode + Anvil init/increment/overflow.
Solana
Typed .sbpf-plan + IDL. No sBPF object yet.
NEAR
raw-u64 Counter/Accumulator WAT/Wasm via wat2wasm.
Noir
Target-owned Plan → .nr packages. No proof/VK.
No silent fallback.
A failure never becomes a success. Stable diagnostics over guessing.
A compiler, not a runtime.
Equivalent materialization
Target only changes artifacts and encoding. Integer semantics, state transitions, revert, call order, authorization and disclosure stay identical.
Fail closed
When semantics cannot be preserved, refuse with a stable diagnostic. No best-effort, no legacy path.
No implicit network
Build performs no network or key IO. Deploy, prove and verify are explicit commands only.