Lean 4 · 多目标编译器

一份可移植程序。跨执行平台的受控物化。

用 Lean 写一次。推导需求。物化到 EVM、Solana、NEAR、Noir、Aleo 等——无法保持语义时拒绝。

开发指南文档

开发指南

环境、写程序、构建命令与 fail-closed 语义。

打开

开放名单

各链成熟度：EVM/Solana 领先；形式化仍在攻关。

打开

目标矩阵

DSL 能力 × 链的覆盖格子。

打开

产品

是编译器——不是链、钱包或隐藏运行时。

ProofForge V2 是 Lean 4 多目标编译器。使用方式见 /docs。 /docs.

一份可移植源码

作者只写一份 program … where。源码不含平台标签——由 target 决定物化，不改业务语义。

语义不可妥协

切换 --target 只能改制品与编码。整数语义、状态迁移、回滚、调用顺序与授权保持不变。

不确定就拒绝

平台无法保持语义时，编译器给出稳定诊断并停止。禁止静默降级与旧路径回退。

语言

写一次。选目标。

在一份 program … where 中描述 state、init、entry 与 view。需求由编译器推导；物化由 --target 选择。

源码不绑定平台标签
SupportClaim 精确匹配——fail closed
文档：指南 · 开放名单 · 矩阵 · Aleo

Examples/Counter.lean

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