What already exists
The NEAR work contributed the first three formal anchors, now onmain:
| Anchor | Module | What it gives us |
|---|---|---|
| Executable IR semantics (scalar subset) | ProofForge/IR/Semantics.lean | A small-step/trace interpreter for the scalar IR subset that proofs can reference; used by the NEAR trace obligations |
| Ownership rules | ProofForge/IR/Ownership.lean, Tests/IROwnership.lean | Checker for release/owned-local discipline (no use-after-release, branch consistency), currently validated by tests |
| Backend trace obligations | ProofForge/Backend/WasmNear/Refinement.lean, ProofForge/Backend/Evm/Refinement.lean, ProofForge/Backend/Evm/YulSemantics.lean, Tests/NearWasmFormal.lean | TraceObligation with decide-checked theorems: the Counter, ValueVault, and EvmExpressionProbe IR traces match expected observable values, EmitWat exports cover the trace entrypoints, the EVM Yul surface contains selector-dispatched functions for the same traces, and the focused emitted Yul subset executes to the same observable EVM return traces |
Verification targets, in priority order
FV-1: Capability routing soundness (small, high value)
ProofForge.Target.requireCapabilities and resolveSpec are the platform’s
core promise: a contract that routes to a target only uses capabilities that
target supports. Today this is a runtime check exercised by tests.
Prove, for the checked boundary:
- Soundness: if
resolveSpec profile spec = .ok plan, then every capability inplan.callsis inprofile.capabilities. - Completeness of rejection: if the spec references a capability outside
the profile,
resolveSpecreturns.error. - Target-extension isolation: if any call carries
solana.*metadata and the profile family is not.solana, resolution fails (D-027 enforced by theorem, not convention).
FV-2: IR semantics coverage and metatheory
ExtendIR/Semantics.lean from the scalar subset toward the checked IR
surface (maps, fixed arrays, structs, ifElse, boundedFor, events as
observable trace items), then state:
- Determinism: evaluation of a well-formed entrypoint body is deterministic (one trace per input/state).
- Progress/preservation for the typed subset: statements that pass the existing shape/type validation do not get stuck and preserve binding types.
- Bounded termination:
boundedForwith static bounds always terminates (structurally true today; state it so future IR changes cannot break it).
decide-friendly) so CI checks stay cheap.
FV-3: Ownership/release soundness (connect FV-2 to IR/Ownership.lean)
The ownership checker currently passes 6 behavioral test cases. Once FV-2
gives release-aware semantics, prove: programs accepted by the ownership
checker never evaluate a released local and never release twice. This is the
formal justification for lowering release to allocator frees in EmitWat
while EVM/Psy reject it and TS ignores it — three different lowerings of one
IR construct are only safe if the IR-level discipline is proven.
FV-4: Backend refinement obligations, one scenario at a time
Replicate theTraceObligation pattern per backend against the shared
scenario (Counter first, ValueVault second):
| Backend | Obligation shape | Feasibility |
|---|---|---|
wasm-near / EmitWat | Exists (exports + IR trace); extend to Wasm-level evaluation of the emitted WAT through the offline host | High — offline host already executes the artifact deterministically |
evm (IR → Yul plan) | Counter, ValueVault, and EvmExpressionProbe obligations exist for IR trace + selector-dispatched Yul surface + executable Yul-subset trace (calldataload, calldatasize, sstore, sload, scalar arithmetic, exp, bitwise/shift operators, comparisons, casts, assertions, number, keccak256, log0-log4, mstore, return); next, extend beyond scalar/assertion coverage into maps, arrays, structs, and aggregate return/state shapes | Medium — the focused Yul-subset interpreter is in Lean; expanding coverage keeps solc out of the trusted path but not out of the build |
psy-dpn | Compare dargo execute result vectors against IR trace outputs (differential gate, not a theorem) | Already close: smoke scripts assert result_vm values today |
solana-sbpf-asm | Differential testing via Mollusk/Surfpool first; assembly-level semantics is a research track, not a near-term proof | Low for proofs, high for differential gates |
wasm-cloudflare-workers | Differential HTTP-level gate only (off-chain host, D-033) | Not a proof target |
wasm-near already has.
FV-5: Checked arithmetic semantics per target
The SDK’s checked operators (+!, -!, *!, /!) must mean the same thing
on a 256-bit EVM word, a 64-bit Wasm integer, and a field element in Psy.
State the intended semantics once in FV-2’s value domain (trap on overflow /
division-by-zero as trace outcomes), then make each backend’s lowering
obligation include the overflow branch. The EVM and Psy diagnostic suites
already test rejection paths; the theorems pin down accepted-path behavior.
FV-6: Lowering equivalence for the two authoring surfaces
contract_source (Lean SDK) and the legacy .learn parser both lower to
ContractSpec. Today equivalence is enforced by paired fixtures. For the
covered subset, prove that parsing a .learn fixture and elaborating the
matching contract_source block produce equal ContractSpec values
(decidable equality already derives). This keeps the “Learn is frozen
compatibility, not a second language” policy honest, and makes drift a build
failure instead of a review judgment.
FV-7: Token SDK plan invariants
TokenSpec.planForTarget invariants worth stating as theorems:
- Feature routing is total: every accepted feature set yields a plan or a planner diagnostic (no silent drops).
- Documented incompatibilities (e.g.
transfer_fee+non_transferable) always produce the diagnostic. - Solana plans reference only program ids and accounts declared in the plan itself (well-formedness of the emitted instruction sequence).
FV-8: User-level contract invariants (product direction)
The long-term differentiator: let contract authors state invariants next tocontract_source (e.g. balance = deposits - releases + fees for
ValueVault) and prove them against the FV-2 semantics before codegen. This
needs no backend work — it is pure Lean over the IR semantics — and is the
first proof surface users see. Start with ValueVault as the worked example.
Non-goals
- No proofs about
solc,wat2wasm,sbpf,leo, or chain runtimes; those stay in the differential-testing trust boundary and are recorded per gate in validation-gates.md. - No proof-transport to chains (no on-chain verification of Lean proofs); proofs gate codegen, per RFC 0001.
- No attempt to verify the Lean elaborator or Lake; the trusted computing base is stated, not eliminated.
Suggested sequencing
- FV-1 capability soundness (structural, unblocks nothing, high trust value).
- FV-2 semantics extension + determinism (foundation).
- FV-3 ownership soundness (justifies the merged
releaselowerings). - FV-4 EVM Yul-subset trace obligations for Counter, ValueVault, and EvmExpressionProbe: done for selector-dispatched scalar-storage and assertion/expression paths; next expand the interpreter and obligations toward maps, arrays, structs, and aggregate return/state shapes.
- FV-6 authoring-surface equivalence for the fixture subset.
- FV-5 / FV-7 as the respective surfaces stabilize; FV-8 once FV-2 lands.