2026年11月4日，系统编程语言项目 Evergreen 上线官方网站与浏览器端 WebAssembly 编译器演练场，直接打出比 C 更强大、比 Rust 更安全的口号。这门新语言试图把显式代码契约、精细的内存状态追踪以及零运行开销的形式化证明塞进同一个编译器前端。口号足够响亮，但翻开其关联的开源仓库 jordan-bonecutter/evergreen 就会发现一个反差事实，这门号称比 Rust 更安全的语言，目前的自举编译器恰恰是用 Rust 写出来的，且距离全链路的可证明安全还隔着几道工程高墙。
契约与内存平面的原生合流：Evergreen 到底改了什么
过去几年，操作系统内核、密码学库和嵌入式基础设施团队一直困在底层控制力与安全保障的拉扯中。C 语言给足了内存控制权，却没有任何安全护栏；Rust 靠所有权与借用检查器在不引入垃圾回收的前提下解决了内存安全，但面对底层侵入式数据结构时仍需退回 unsafe，且标准类型系统无法直接证明业务逻辑里没有算术溢出或数组越界。
Evergreen 的核心动作是把形式化验证从外部插件变成语言的出厂设置。根据官方演练场展示的机制，它将三项能力合入了同一套语法：
- 契约与不变量直接写在代码旁，通过
where声明前置条件与类型约束（例如定义非零类型NonZero时要求输入不等于 0），用ensures声明后置条件，全部变成编译器必须检查的证明义务。 - 引入内存平面（memory planes）机制追踪显式布局、所有权与借用引用，例如通过可变引用
*cell = 10修改变量后，编译器能直接推导出原变量值等于 10 的静态事实。 - 提供零性能开销的形式化证明，允许开发者编写归纳引理与
ideal理想数学计算（如将机器类型usize转为理想整数比对 42），所有证明与幽灵计算在编译检查通过后会被彻底擦除，不拖累最终二进制文件的执行效率。
这种设计直接回应了高保障软件领域的路线分歧。此前行业要么选用 Dafny、F* 这类验证导向语言，代价是系统级生态狭窄；要么在 Rust 之上挂载 Verus、Creusot 或 Kani 等验证工具，复用生态却要在借用编码与语法摩擦上交学费。Evergreen 选择了推倒重来，试图在编译器前端把内存安全检查与定理证明合二为一。
拆开 GitHub 源码：内存平面的取舍与信任链缺口
只看官网不到 20 行的演示代码，很容易以为出现了一套全面碾压 Rust 借用检查器的底层数学魔法。但深入检视其开源仓库与自举文档（docs/bootstrap.md），工程现实与营销口号之间的温差立刻显现出来。
项目文档明确将当前已实现的自举编译器与原始语言设计草图做了切割，承认原始设计中的部分特性尚未落地。更核心的机制差异在于，Evergreen 在编译期并没有调用外部定理证明器 Lean，而是依靠自带的内部验证器（src/compiler/verify.rs）、证明内核（src/compiler/kernel.rs）以及证明证书与重放模块（src/compiler/certificate.rs）完成闭环检查。
在最受关注的内存平面实现（src/shared/mod.rs）上，Evergreen 做出了鲜明的工程妥协：
- 对于普通内存操作同布局的标量写入或替换可以保留现有引用；一旦发生移动、释放或改变布局的替换，受影响的引用就会失效，即便重新初始化已移动的槽位也不会复活旧引用。
- 针对堆内存所有权Evergreen 引入了极有亮点的
unique(T)机制，使其持有独立且稳定的数据平面。这意味着移动所有者本身仍能保留对其堆载荷的借用，只有真正释放分配时借用才会失效，直接端掉了 Rust 自引用结构与所有权转移时的常见痛点。 - 但在处理复杂数据结构时当前的自举编译器对聚合体采取了保守简化策略，将其整体视为单一内存平面。结果是修改结构体局部字段时，可能会连带使其中原本无关的其他引用一并失效。在字段级拆分借用这一高频场景上，它目前的实际表现反而比 Rust 借用检查器更加严苛。
源码契约的数学自洽，还不等于机器码的绝对可信。
更严肃的限制在于可信计算基（TCB）的边界。形式化验证研究早就表明，即便源码规约逻辑被证明成立，从验证条件生成到可执行二进制文件的转译链条仍存在信任缺口。Evergreen 仓库 proofs/*.lean 目录下的 Lean 规范，目前仅针对 unique(T) 等局部语义提供独立的数学模型和人工审查制品；官方文档坦承，这些模型并未证明完整编译器或内存分配器的正确性。
放在 Verus 与 Creusot 坐标系下，谁该关注它
评价 Evergreen 宣称的比 Rust 更安全，必须先对齐参照系。普通 Safe Rust 的设计目标是内存安全与无数据竞争，本来就不包办业务逻辑正确性；Evergreen 靠精化类型与前后置契约确实比裸写 Rust 多拦截了算术与逻辑错误，但真正的同行对手是 Rust 加上 Verus 或 Creusot 的组合。
在现有 Rust 验证生态里，Verus 与 Creusot 已经能为代码附加规约并证明功能属性。例如 Creusot 通过转译至 Why3 架构严格区分机器整数与数学整数，且默认只提供部分正确性证明（即在假设函数终止的前提下证明后置条件成立）。相比之下，Evergreen 把 ideal 理想计算和证书重放内核直接下沉到原生语法，确实省去了外部工具链拼装的繁琐，但它同样要面对形式化验证绕不开的两大难关：一是如何严密限制递归规范函数的终止性以防逻辑不健全，二是一旦离开官网 10 行以内的 increment 玩具代码，程序员需要手写多少归纳引理才能让编译器放行。
截至目前，Hacker News 与 Reddit 等技术社区尚无针对 jordan-bonecutter/evergreen 的独立基准测试与生产验证讨论；由于社区里同时存在另一个 2026 年 10 月发布的同名 Rust 编写项目 Evergreen Common Lisp（atgreen/evergreen），检索时还极易发生命名混淆。
- 风险.Evergreen 尚处于用 Rust 编写的自举阶段，聚合体内存平面过于保守且缺乏完整编译器验证，任何生产环境当前都不应将其纳入技术选型或迁移预算。
对于真正手握预算的操作系统内核与密码学研发团队而言，现阶段最务实的动作依然是守住 Rust 配合 Verus 或 Kani 的渐进式验证防线。但 Evergreen 给编程语言设计者和形式化验证工具维护者提供了一个极佳的实验样本。接下来判断它能否走出玩具阶段，只需盯紧三个硬指标：聚合体内存平面何时支持细粒度字段投影、何时摆脱 Rust 实现编译器自举，以及在重写内存分配器这类真实系统组件时的证明代码比究竟能压到多低。