01
重复实现
每个平台重写一次业务逻辑，维护成本随链数线性上升。
proof-forge-next · Lean 4 · Phase 1
一份业务程序，多种链上制品。
语义不支持，就拒绝编译。
ProofForge 是用 Lean 4 实现的多目标编译器。作者只写一份 portable program；编译器推导语义需求，再按 --target 物化到 EVM、Solana、NEAR、Noir——无法等价实现时给出稳定诊断并拒绝，禁止静默降级。
- Phase 1 目标
- 4
- 核心不变量
- INV
- 运行时?
- 否
问题
多链开发最贵的不是写代码，是语义漂移。
同一业务逻辑若要分别在 EVM、Solana、NEAR、ZK 电路上实现，通常意味着多套源码、多套测试，以及「看起来一样、边界行为却不同」的风险。ProofForge 把业务语义固定在一份 target-neutral 源码里，让平台差异只出现在物化层。
02
静默不一致
整数溢出、回滚、授权、调用顺序在不同链上常被「近似实现」。
03
虚假成功
best-effort 编译看似通过，却悄悄改变了程序语义。
方案
写程序，不写「链方言」。
源码描述状态、入口与视图；类别（合约 / 电路 / Wasm 宿主）由 --target 决定，不得偷偷改业务语义。
单源多目标
一份 program … where，可对多个执行平台生成受控制品。
需求驱动
编译器从源码推导 ProgramRequirements，再与目标能力精确匹配。
Fail-closed
目标无法支持时必须拒绝并给出稳定诊断，禁止 fallback。
非运行时
编译器只做代码生成与语义检查；不托管密钥、不隐式联网部署。
30 秒上手
同一份 Counter，切换 target 只改制品。
下面是 README 中的示例程序。选择目标平台，查看会生成什么——以及当前阶段的诚实成熟度。
选择 target
源码 · portable
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 count命令
lake env .lake/build/bin/proof-forge-next build \
Examples/Counter.lean \
--module Examples.Counter \
--target solana -o build/counter-solana物化结果 · solana
.sbpf-plan + IDL
typed .sbpf-plan + IDL；无 sBPF/ELF/runtime
Phase 1编译管线
从语法到制品：每一步可拒绝。
Syntax 只是入口，不是领域语义。失败路径 fail closed——不允许降级到 legacy 成功路径。
- 01ParseLean Syntax → 可移植源
- 02Typed名称 / 类型 / 效果
- 03Semantic需求抽取
- 04Resolve精确 SupportClaim
- 05Materialize目标 Plan / IR
- 06Emit原子写出 + 溯源
目标与成熟度
诚实标注，不夸大。
Phase 1 四个后端均有可测证据；设计中的平台不宣称产品能力。
evm
Phase 1合约 VM
Counter bytecode + Anvil 测试；非完整 EVM 后端
solana
Phase 1显式账户 SVM
typed .sbpf-plan + IDL；无 sBPF/ELF/runtime
near
Phase 1Wasm 宿主
WAT/Wasm 输出；无 sandbox receipt
noir
Phase 1电路
.nr 包；无 Nargo/ACIR/proof/VK
CosmWasm / Soroban / ICP 等仅在设计与研究阶段，无产品后端宣称。
不变量
编译器对自己诚实。
核心不变量约束整个管线——源码层不按目标分支，目标只能做等价物化。
INV-001
目标中立前端
Source / Typed / Semantic 层不按 TargetId 分支。
INV-002
等价物化
target 只能做语义等价的物化；否则拒绝。
INV-005
失败即失败
任一失败不得变成「成功」或 legacy fallback。
INV-008
无副作用构建
build 无网络与密钥副作用；deploy / prove / verify 必须显式。
明确边界
ProofForge 不是什么。
- 不是链上 VM 或完整协议实现
- 不自动部署、不接触私钥或默认 RPC
- 不把任意 Lean 项混入 DSL 绕过检查
- 第一阶段不宣称生产就绪或审计完成