Skip to main content
Status: Accepted Date: 2026-06-30

​
Summary

ProofForge should evolve from an EVM backend experiment into a Lean-first multi-chain contract platform. Developers write contract business logic, state-machine rules, and proofs in Lean. At build time they choose a target chain family, and ProofForge produces target-specific artifacts, tests, and deployment packages. The first architecture decision is to use a portable core plus capabilities model:
  • Portable core: pure business logic, arithmetic, state-machine transitions, invariants, and proofs that should stay chain-independent.
  • Capabilities: explicit chain-facing operations such as storage, caller identity, value transfer, events, cross-contract calls, account access, object/resource access, and chain environment reads.
  • Target adapters: ABI, artifact, test runner, deployment, and host-runtime glue for a specific chain family.
This model avoids pretending that EVM, Solana, Wasm chains, Move chains, ZK/circuit targets, and Bitcoin-like systems have identical semantics. The goal is not a weakest-common denominator language. The goal is one verified business core with clear, auditable target boundaries.

​
Current Baseline

The repository currently has an EVM baseline: 
Lean contract
  -> Lean frontend / LCNF
  -> EmitYul
  -> Yul
  -> solc --strict-assembly
  -> EVM runtime bytecode
  -> Foundry smoke tests
Implemented today:
  • ProofForge.Evm: EVM SDK primitives and typed helpers.
  • ProofForge.Compiler.LCNF.EmitYul: LCNF to Yul lowering.
  • proof-forge --evm-bytecode: EVM bytecode CLI mode.
  • .evm-methods: method dispatch metadata for ABI selectors.
  • Foundry smoke tests using generated runtime bytecode.
Not implemented today:
  • A target-independent contract IR.
  • Solana/sBPF, Wasm-family, Move-family, or ZK/circuit backends.
  • Cloud build, deployment, artifact registry, or hosted testnet flows.

​
External Landscape

The multi-chain contract space has related projects, but no dominant Lean-first verified multi-chain deployment platform.
AreaReferenceRelevance
Multi-chain languageReach, https://www.reach.sh/Closest high-level precedent for writing an application once and deploying to multiple chains.
Solidity multi-target compilerSolang, https://solang.readthedocs.io/Shows that one source language can lower to non-EVM blockchain targets, but starts from Solidity rather than Lean/proofs.
EVMFoundry and solc toolchainsMature local testing and bytecode pipeline; current ProofForge baseline.
SolanaPrograms docs, https://solana.com/docs/core/programsHigh-value target with an account/instruction model very different from EVM.
Wasm chainsNEAR, https://docs.near.org/smart-contracts/what-isWasm contract model with chain-specific host ABI and account model.
Wasm chainsCosmWasm, https://cosmwasm.cosmos.network/Wasm contracts across Cosmos chains with a distinct message/storage model.
Wasm chainsink!, https://use.ink/docs/v5/why-webassembly-for-smart-contracts/Polkadot/Substrate smart contracts via Wasm.
Move chainsSui Move, https://docs.sui.io/concepts/sui-move-conceptsObject/resource semantics, strong type discipline, and a Move VM target family.
Move chainsAptos smart contracts, https://aptos.dev/en/build/smart-contractsMove module/resource model with a separate account and deployment model.
ZK/circuit targetsPsy compiler, https://github.com/PsyProtocol/psy-compilerZK-oriented contract compiler that emits DPN circuit function definitions rather than EVM-style bytecode.
Bitcoin ecosystemStacks Clarity, https://docs.stacks.co/learn/clarityBitcoin-adjacent smart contract language with decidability goals.
Bitcoin ecosystemBitVM, https://bitvm.org/Research direction for Bitcoin computation verification, not a direct first backend target.

​
Target Architecture

                 +---------------------------+
                 | Lean contract + proofs    |
                 +-------------+-------------+
                               |
                               v
                 +---------------------------+
                 | Lean frontend / LCNF      |
                 +-------------+-------------+
                               |
                               v
                 +---------------------------+
                 | Portable Contract IR      |
              +------+------+------+------+------+
                     |      |      |      |      |
                     v      v      v      v      v
                  +-----+ +-------------+ +-------------+ +-------------+ +--------+
                  | EVM | | Solana/sBPF | | Wasm family | | Move family | | ZK/DPN |
                  +-----+ +-------------+ +-------------+ +-------------+ +--------+
                     |          |              |               |             |
                     v          v              v               v             v
                 Yul/solc  Solana program  NEAR/CosmWasm  Sui/Aptos     Psy/DPN
                                           Polkadot/ink!
The portable IR must sit above target ABI details and below Lean source syntax. It should represent:
  • Exported contract entrypoints and method metadata.
  • Portable values, structs, enums, arrays, maps, and errors.
  • State transition functions and declared invariants.
  • Capability calls as typed effects rather than raw target opcodes.
  • Proof-carrying facts that can be checked before backend lowering.
Target backends lower this IR to each chain family:
  • EVM backend: Yul object, ABI selector dispatch, solc bytecode, Foundry tests.
  • Solana backend: sBPF package, instruction dispatch, account metadata, PDA helpers, CPI boundaries, Solana local validator tests.
  • Wasm backend family: shared Wasm lowering plus chain-specific host ABI adapters for NEAR, CosmWasm, and Polkadot/ink-style contracts.
  • Move backend family: Move module/package adapters for Sui and Aptos, with a research phase for direct Move bytecode or generated Move source.
  • ZK circuit backend family: target source generation plus target-native circuit artifact generation, starting with Psy/DPN.

​
Capability Model

Portable code must not call raw EVM, Solana, Wasm, Move, or ZK VM host APIs directly. It calls ProofForge capabilities. Each target declares which capabilities it supports and how they lower. Initial capability groups:
CapabilityPortable meaningTarget notes
StorageRead/write contract stateEVM slots, Solana accounts, Wasm storage, Move resources/objects differ significantly.
CallerIdentify transaction signer/callerEVM caller, Solana signer account, Wasm sender, Move transaction sender.
ValueNative token movement or received valueNot all chains expose EVM-style msg.value; adapters must make this explicit.
EventsEmit indexed or structured outputEVM logs, Solana logs/events, Wasm events, Move events.
Cross-callCall another contract/program/moduleEVM calls, Solana CPI, Wasm messages/promises, Move module calls.
Time/envBlock height, timestamp, chain idAvailability and finality semantics vary by target.
CryptoHashing, signature recovery, precompilesSome targets expose host functions, others require library lowering.
Account/object/resourceChain-native state containersEspecially important for Solana accounts and Move objects/resources.
ZK/circuitCircuit artifact generation and proof flowEspecially important for Psy/DPN and future ZK VM targets.
The compiler should reject a target build when a contract uses unsupported capabilities. Rejection is preferable to silently changing semantics.

​
CLI And Product Surface

The future local CLI should expose target selection as the stable public interface: 
proof-forge build --target evm --out build/evm
proof-forge build --target solana-sbpf-asm --out build/solana
proof-forge build --target wasm-near --out build/near
proof-forge build --target wasm-cosmwasm --out build/cosmwasm
proof-forge build --target move-sui --out build/sui
proof-forge build --target move-aptos --out build/aptos
proof-forge build --target psy-dpn --out build/psy-dpn
Polkadot/ink-style contracts (wasm-polkadot) remain research-only until a target profile and spike are scheduled. See decisions.md. Psy/DPN (psy-dpn) is now Experimental for a restricted portable IR subset: generated .psy source plus Dargo, not a public Yul-like IR, remains the integration route. The current proof-forge --evm-bytecode mode remains the EVM baseline until the target-oriented build command exists. Future cloud platform surface:
  • Import from GitHub.
  • Select target matrix.
  • Run deterministic builds in isolated workers.
  • Run target-native local/testnet smoke tests.
  • Store artifacts, ABIs, proofs, deployment metadata, and verification reports.
  • Deploy to configured testnets/mainnets after explicit signing or wallet approval.
  • Show a Vercel/Cloudflare-like project dashboard with builds, environments, deployments, logs, and chain-specific health checks.

​
Roadmap

​
Phase 0: EVM baseline

Status: implemented in this repository.
  • Keep EVM examples compiling through proof-forge --evm-bytecode.
  • Keep Foundry smoke tests as the mature EVM test harness.
  • Treat current EVM SDK primitives as the first concrete capability source.

​
Phase 1: Target model and portable IR

  • Introduce a target registry and target identifiers.
  • Split EVM-specific SDK calls from portable contract capabilities.
  • Define the portable contract IR (spec) and artifact metadata.
  • Add compile-time errors for unsupported target capabilities (registry).
  • Define the Counter shared scenario.

​
Phase 2: Parallel target spikes (CosmWasm + Solana)

Requires Phase 1 complete. CosmWasm and Solana spikes may proceed in parallel. CosmWasm (wasm-cosmwasm):
  • Wasm-host adapter with region ABI and JSON messages.
  • Counter smoke through cosmwasm-check.
Solana (solana-sbpf-linker):
  • Map portable entrypoints to instruction dispatch with explicit accounts.
  • Produce a minimal sBPF artifact via stock Zig + sbpf-linker.
  • Run under Mollusk or Solana local validator.
Both spikes use the same portable IR Counter module. See decisions.md.

​
Phase 3: Move family

  • Generate Move source from restricted portable IR (Aptos POC first, then Sui).
  • Model Sui objects and Aptos resources as target capabilities.
  • Validate Counter (or successor scenario) on EVM and Aptos.

​
Phase 3.5: ZK circuit target research

  • Generate Psy-compatible .psy source from restricted portable IR.
  • Compile through Dargo to DPN circuit JSON.
  • Decide whether in-memory Psy execution is sufficient before local node/prover deployment smoke.

​
Phase 4: Cross-target scenario hardening

  • Shared scenario tests across EVM and at least two non-EVM targets.
  • Golden IR and artifact snapshots.
  • Capability matrix coverage for Counter v1 (events, access control optional).

​
Phase 5: Cloud platform

  • Add hosted target-matrix builds.
  • Add artifact registry and deploy history.
  • Add testnet deployment flows.
  • Add verification reports that show proof status, target capabilities used, and chain-specific warnings.

​
Non-goals

  • Do not promise that every contract compiles to every chain.
  • Do not hide chain economics, finality, account models, or resource models.
  • Do not translate arbitrary EVM bytecode to every target.
  • Do not target Bitcoin L1 execution as an early backend.
  • Do not replace mature target-native tools such as Foundry, Solana local validator tooling, NEAR tooling, CosmWasm tooling, or Move CLIs. Integrate with them first.

​
Testing Strategy

Every target family should have four test layers:
  • Lean checks: proofs, pure logic, and state-machine invariants.
  • Golden artifacts: stable IR and backend output snapshots for small examples.
  • Target-native smoke tests: Foundry for EVM, Solana local validator for sBPF, chain-specific Wasm runners, Move local/testnet tooling, and Dargo/Psy tooling for psy-dpn.
  • Cross-target scenario tests: the same portable contract scenario should produce equivalent high-level outcomes across supported targets.
CI should start with EVM only, then expand into a target matrix as new backends land. A target is not considered supported until it has at least one local smoke test and one shared portable scenario test.

​
Open Questions

  • How much of Lean’s LCNF should be preserved in the portable contract IR?
  • Should target adapters be written in Lean only, or can some adapters use Zig/Rust/Go when chain tooling makes that more reliable?
  • For Move, is generated Move source acceptable for the first backend, or is direct Move bytecode required for the platform story?
  • For Wasm, should the compiler emit one generic Wasm core plus adapters, or separate Wasm per chain from the beginning?
  • How should cloud deployment handle private keys, multisig workflows, and user-controlled signing?