编程 Vera 深度拆解：当编程语言学会「为LLM而生」——无变量名、强制契约、SMT证明的代码验证新范式

2026-07-15 19:14:48 +0800 CST views 11

Vera 深度拆解：当编程语言学会「为LLM而生」——无变量名、强制契约、SMT证明的代码验证新范式

前言

2026年7月，一个名为 Vera（发音 v-ERR-a）的编程语言悄悄上线 GitHub，在短短一周内获得了极高的关注度。这个语言的名字来自拉丁语 veritas（真理），它的核心理念却极其颠覆：不是为人设计的，而是为大型语言模型设计的。

这句话的分量有多重？我们需要回顾一下编程语言的历史——汇编语言诞生于硬件约束，C语言诞生于操作系统需求，Python诞生于生产力需求。每一次编程语言的进化，都是为了服务它最重要的用户群体。而今天，如果模型成为代码的主要编写者，那么语言是否也应该适应这一变化？

Vera 给出了它的答案。

在深入技术细节之前，让我们先理解一个根本问题：LLM写代码时最大的问题是什么？ Vera 的设计者引用了大量实证研究（包括 arXiv:2307.12488），结论出人意料：不是语法，而是规模化的连贯性。模型擅长局部模式匹配，但在维护跨代码库的全局不变式、理解变更的连锁反应、追踪随时间变化的状态时极其脆弱。尤其是在命名方面——选择误导性名称、错误地重复使用名称、丢失名称与值的追踪——这是模型最常见的错误类型。

Vera 的解法是：不要求模型正确，只要求模型可检查。 变量名被结构化引用取代，契约是强制的，效果是类型化的，每个函数都是编译器可以验证的规范。

本文将从工程师视角，深度拆解 Vera 的架构设计、核心语言特性、编译器实现，以及它对整个编程语言生态可能带来的深远影响。

一、背景：为什么我们需要一门为LLM设计的语言？

1.1 从「人来写」到「模型写」的根本转变

传统编程语言的设计哲学是以人为中心的：变量要有意义的名字，注释要解释意图，代码风格要有可读性，IDE 要提供智能提示。这些设计的共同假设是：代码最终由人类阅读和维护。

然而，当模型成为代码的主要编写者时，这个假设不再成立：

局部最优陷阱：模型是模式匹配器，优化的是局部合理性而非全局架构。随着代码规模增大，模型的「上下文窗口」压力增大，连贯性急剧下降。
命名幻觉：模型可以生成语法正确的代码，但变量名、函数名的选择可能完全误导人类读者。比如同一个概念在不同地方用了三个不同的名字，模型自己并不觉得这有问题。
状态追踪困难：模型在处理可变状态、副作用、并发时尤其脆弱，因为它本质上是在「预测」下一个 token，而非「理解」系统状态。

1.2 现有语言的局限性

我们已经有了许多强大的验证性语言——Dafny、Lean、Koka、F*——它们都有契约系统、证明助手或效果类型。但这些语言的设计初衷是让人更高效地编写正确代码，而不是让模型编写可验证代码。

举例来说：

Dafny 的契约是可选的，不是强制的
Lean 需要人工编写真证明
Koka 的效果系统复杂，学习曲线陡峭
F* 定位为研究语言，生产级工具链不完善

这些语言在模型手中时，模型可以选择性忽略契约、写出难以证明的代码、使用复杂语法导致错误率上升。

Vera 的目标是：设计一门模型无法绕过的语言。 所有契约都是强制的，效果必须显式声明，代码的正确性是可机械验证的。如果代码有错误，编译器给出的不是人类的诊断信息，而是给模型的修复指令。

二、核心设计原则：六条铁律

Vera 的设计文档（DESIGN.md）明确定义了六条设计原则，每一条都直接针对 LLM 的弱点：

原则一：可检查性优先于正确性

代码必须能机械地检查。当出错时，编译器提供自然语言解释和具体修复方案——这是一条指令，不是一份状态报告。

这意味着 Vera 不追求「让代码写出来就是对的」，而是追求「让错误的代码无法通过检查」。

原则二：显式性优先于便利性

所有状态变更必须声明，所有效果必须类型化，所有函数契约必须存在。没有隐式行为。

原则三：单一规范形式

每个语法构造只有一种标准表示，没有风格选择，没有 linter 的存在空间。消除格式风格的分歧，让模型专注于逻辑而非格式。

原则四：结构化引用替代名称

绑定通过类型和位置索引（@T.n）引用，而非任意名称。这直接解决了模型最脆弱的命名问题。

原则五：契约是真理的来源

每个函数声明它需要什么（requires）、保证什么（ensures）。编译器静态验证，在可行的地方用 SMT 证明。

原则六：受限的表达力

更少的有效程序 = 更少的模型犯错机会。Vera 刻意限制了语言可以表达的东西，强制使用 ADT、match、函数式集合操作。

三、语言核心特性深度解析

3.1 无变量名：@T.n 结构化引用

这是 Vera 最具争议也最核心的设计决策：没有变量名，所有绑定通过类型和位置索引引用。

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}

解释一下：

@Int 是类型
@Int.0 是最近的一个 Int 绑定
@Int.1 是倒数第二个 Int 绑定
@Int.result 是函数返回值（由 ensures 引入）

这实际上是 de Bruijn 索引在编程语言中的直接应用。de Bruijn 索引是 lambda 演算中避免命名冲突的标准技术，Vera 将其扩展到了所有绑定。

为什么这对 LLM 如此重要？ 当模型写代码时，最常见的错误之一就是「名字冲突」——在不同的作用域内使用了相同的变量名，或者在不同位置引用了错误的变量。通过结构化索引，Vera 完全消除了这类错误的可能性。模型不需要「记住」哪个名字指哪个值，只需要知道位置关系。

3.2 强制契约：SMT 静态证明

Vera 的每个函数必须包含三部分契约：

requires：前置条件，编译器在每个调用点用 Z3 SMT 求解器静态证明。如果无法证明，编译失败。

ensures：后置条件，同样由 SMT 求解器证明。

effects：效果声明，函数是否有副作用（pure = 无任何副作用）。

看一个更复杂的例子：

public fn safe_access(@Array<Int>, @Nat -> @Result<Int, Error>)
  requires(array_length(@Array<Int>.0) > @Nat.0)
  ensures(true)
  effects(pure)
{
  let @Result<Int, Error> = Array.at(@Array<Int>.0, @Nat.0);
  match @Result<Int, Error>.0 {
    Some(@Int) -> Ok(@Int.0),
    None -> Err(InvalidIndex)
  }
}

这里 requires(array_length(@Array<Int>.0) > @Nat.0) 确保数组访问不会越界。如果 SMT 求解器能证明这个条件在所有调用点都成立，那么运行时不需要边界检查。如果无法证明（比如数组长度是动态的），编译器会插入运行时边界检查。

三层验证体系：

层级	机制	条件
Tier 1	Z3 静态证明	SMT 可判定时，编译期证明
Tier 2	Z3 引导的运行时	SMT 半可判定时（尚未实现）
Tier 3	运行时守卫	SMT 不可判定时，运行时 trap

对于除零运算，Tier 1 → 编译期报错（E526）；对于可证明越界的数组访问 → 编译期报错（E527）；对于运行时才能确定的情况 → 运行时边界检查。这意味着：任何通过 vera verify 的运算，对所有输入都是安全的。

3.3 效果类型系统：副作用无所遁形

Vera 默认是纯函数式的。如果函数要调用外部世界，必须在签名中声明效果：

public fn research_topic(@String -> @Result<String, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Http, Inference>)
{
  let @Result<String, String> = Http.get(
    string_concat("https://search.example.com/?q=", @String.0));
  match @Result<String, String>.0 {
    Ok(@String) -> Inference.complete(
      string_concat("Summarise this research:\n\n", @String.0)),
    Err(@String) -> Err(@String.0)
  }
}

这个函数的效果声明 <Http, Inference> 表示它会发起 HTTP 请求并调用 LLM 推理。如果调用者没有在效果行中声明这些能力，编译器直接拒绝编译。

效果类型系统还支持 mock：

handle[Inference] with mock_inference

在测试环境中，可以用 mock 实现替换真实 LLM 调用，使得测试完全确定性。

3.4 错误处理：Result 与 Exn 双轨制

Vera 使用两种错误处理机制：

Result<T, E>：用于已知、可恢复的错误类型。模型必须用 match 处理所有情况，否则编译器报错（穷尽性检查）。

public fn parse_number(@String -> @Result<Int, ParseError>)
  requires(true)
  ensures(true)
  effects(pure)
{
  match String.to_int(@String.0) {
    Ok(@Int) -> Ok(@Int.0),
    Err(@String) -> Err(InvalidNumber)
  }
}

Exn<T>：代数效果，用于异常情况，可在 handler 中统一处理。这是一种更灵活的效果系统，类似于 Koka 或 Eff 语言中的效果处理器。

3.5 数据类型与穷尽性检查

Vera 的数据类型系统基于 代数数据类型（ADT） + 穷尽性 match：

public type @Result<T, E> = Ok(T) | Err(E)
public type @Option<T> = Some(T) | None
public type @List<T> = Cons(T, List<T>) | Nil

任何对 ADT 的 match 必须覆盖所有情况。编译器会强制这一点，模型不能遗漏分支。

3.6 精化类型

Vera 支持在类型层面编码值级约束：

let @Int@{| @Int.0 > 0|} = get_positive_number()

这里的 @{| predicate |} 就是精化类型（Refinement Type）。编译器用 Z3 验证谓词是否成立。超出约束的赋值在编译期就被拒绝。

四、编译器架构：从源码到 WebAssembly

4.1 Python 参考实现

Vera 选择 Python 作为参考实现语言（而非追求性能的 Rust 或 C++）。这是一个刻意为之的决策：正确性优先于性能。编译器代码量少、易于审查、易于实验新优化 passes。

架构上，编译器分为以下几个阶段：

Source Code
    ↓
[Lexing & Parsing]  →  AST
    ↓
[Type Checking]  →  Typed AST + Constraint Generation
    ↓
[SMT Verification]  →  Z3 Constraint Solving
    ↓
[Code Generation]  →  WebAssembly

4.2 Z3 SMT 集成

编译器核心集成了 Microsoft 的 Z3 SMT 求解器。对于每个 requires/ensures 条件，编译器：

将 Vera 表达式翻译为 Z3 的 SMT-LIB2 格式
查询求解器是否能在所有路径上证明条件成立
根据结果生成相应的 Tier 1（静态证明）或 Tier 3（运行时守卫）

# 编译器内部简化逻辑示意
def verify_requires(fn, call_site):
    constraints = build_smt_constraints(fn.requires, call_site)
    result = z3.solve(constraints)
    if result == "unsat":
        # 所有路径都满足，Tier 1，编译通过
        return Tier.ONE_PROVEN
    elif result == "sat":
        # 存在不满足的路径，插入 Tier 3 运行时检查
        return Tier.THREE_RUNTIME_GUARD

4.3 WebAssembly 编译目标

Vera 的最终编译目标是 WebAssembly。这意味着 Vera 程序可以：

在命令行通过 Wasmtime 运行（vera run）
在浏览器中运行（vera compile --target browser 生成 JS bundle）
在标准 WASI Preview 2 主机上运行（vera compile --target wasi-p2 生成 WASI 组件）

这三条路径覆盖了服务端 CLI、浏览器前端、以及新兴的 WASI 边缘计算场景。

为什么选 WebAssembly？

沙盒安全：WASM 运行时没有环境能力（无文件系统、网络等），除非通过 WASI 接口显式授权
可移植性：一次编译，到处运行（浏览器 + 服务器 + 边缘）
性能：WASM 的执行效率接近原生代码
模型友好：WASM 的二进制格式紧凑，下载快，冷启动快

4.4 内存管理与 GC

Vera 在 WASM 中实现了保守式标记-清扫 GC，完全在生成的 WASM 代码内部实现（$alloc、$gc_collect、shadow stack），不依赖宿主机的 GC。这意味着模型在编写 Vera 代码时不需要考虑内存管理，专注于业务逻辑。

五、完整的开发工作流

5.1 安装

python -m venv .venv
source .venv/bin/activate
python -m pip install veralang

# 编辑器支持（LSP）
python -m pip install "veralang[lsp]"

注意：PyPI 上的 vera 包名已被其他项目占用，所以包名是 veralang，命令仍是 vera。

5.2 标准工作流

1. 模型编写 Vera 代码（含强制契约）
2. 模型通过编译器获取错误信息（每条错误都是修复指令）
3. 编译器静态验证（或运行时守卫）
4. 编译到 WebAssembly
5. 在任何 WASM 运行时执行

关键点：第2步的错误信息是给模型看的，不是给人看的。每条错误都包含：

出了什么问题（E526, E527 等稳定错误码）
为什么会出错
如何修复（带具体代码示例）
规范引用（spec 中的具体章节）

5.3 LLM 推理集成

Vera 的 Inference.complete 效果让 LLM 调用成为一等公民：

VERA_ANTHROPIC_API_KEY=sk-ant-... vera run examples/inference.vera

支持的推理提供商包括 Anthropic、OpenAI、Ollama 等。通过效果系统的 mock，测试可以在没有真实 API key 的情况下运行。

六、与其他语言的横向对比

6.1 语法哲学对比

特性	Vera	Rust	Python	Dafny
变量引用	`@T.n`（de Bruijn索引）	名称绑定 + 借用检查	名称绑定	名称绑定
契约	强制，必填	无	无	可选
效果系统	有，代数效果	无（`Result` 枚举）	无	无
SMT验证	内置 Z3	无	无	内置 Z3
编译目标	WebAssembly	Native	Bytecode	.NET/JS
目标用户	LLM	人类工程师	人类工程师	人类工程师

6.2 为什么模型写 Vera 比写 Rust 更可靠？

这个问题值得深入分析。Rust 强大的所有权和生命周期系统确实能消除大量内存错误，但它的复杂性也为模型埋下了大量新的错误来源：

借用检查器是出了名的难以理解，模型的 Rust 代码经常遇到「lifetime mismatch」错误
编译器错误信息虽然详尽，但针对的是人类理解，不是模型修复
语法复杂度高，&、&mut、Box、Rc、Arc、RefCell……模型需要在正确的上下文选择正确的智能指针类型
契约可选，模型可以选择忽略 unsafe 的前置条件

Vera 的优势在于：更少的决策，更明确的约束，更强的验证。模型不是在学习复杂的类型系统技巧，而是在填写规范模板。

6.3 与传统验证语言的对比

Dafny 是 Vera 最接近的参照物——两者都强调 SMT 验证、契约编程、编译到可执行代码。但关键区别在于：

Dafny：契约默认可选，可以写没有契约的 Dafny 代码
Vera：契约强制，没有契约的函数是编译错误

这看起来是 Vera 更严格，但也意味着：Vera 牺牲了快速原型和脚本的能力，换取了「所有代码都可验证」的一致性保证。

七、实际代码示例：从需求到验证

让我们通过一个完整示例，体会 Vera 的开发体验。

场景：实现一个安全的排序函数

第一步：编写合约

public fn safe_sort(@Array<Int> -> @Array<Int>)
  requires(true)
  ensures(
    array_length(@Array<Int>.result) == array_length(@Array<Int>.0)  // 长度不变
    and is_sorted(@Array<Int>.result)                               // 结果有序
    and is_permutation(@Array<Int>.result, @Array<Int>.0)           // 是原始数组的排列
  )
  effects(pure)
{
  // 留空，让模型理解规范的结构
}

第二步：模型填充实现

public fn safe_sort(@Array<Int> -> @Array<Int>)
  requires(true)
  ensures(
    array_length(@Array<Int>.result) == array_length(@Array<Int>.0)
    and is_sorted(@Array<Int>.result)
    and is_permutation(@Array<Int>.result, @Array<Int>.0)
  )
  effects(pure)
{
  // 冒泡排序实现
  let @Int = array_length(@Array<Int>.0);
  let @Array<Int> = @Array<Int>.0;

  let @Int = @Int.0;
  let @Array<Int> = @Array<Int>.0;

  // 外层循环
  for @Int.2 in range(@Int.0) {
    // 内层循环
    for @Int.3 in range(@Int.2, @Int.0) {
      let @Int = @Int.2;
      let @Int = @Int.3;
      // 交换逻辑...
    }
  }
  @Array<Int>.0
}

第三步：编译器报错

[E527] Error at sort.vera, line 18:

    let @Int = @Int.2;
        ^^^^^

  Variable '@Int.2' provably out of bounds.
  The SMT solver proved that @Int.2 is always >= array_length(@Array<Int>).

  Fix:

    Change the range to:
      for @Nat in range(@Nat.0, array_length(@Array<Int>.0)) {
        ...
      }

  See: Chapter 7, Section 7.3 "Loop Bounds and Index Validation"

注意这里的错误信息：不是「索引越界」，而是告诉模型如何修复，甚至给出了具体的代码替换建议。

八、性能优化与工程实践

8.1 SMT 验证的性能考量

Z3 SMT 求解器的性能是编译器设计的关键瓶颈。Vera 采用了以下策略：

分块验证：对于长函数，编译器将约束拆分为多个独立子问题并行求解。

增量求解：利用 Z3 的 push/pop API 复用之前的求解上下文。

启发式超时：对于复杂约束，设置 SMT 超时，超时后自动降级到 Tier 3。

Tier 2 的潜力：Z3 引导的运行时验证（Tier 2）尚未实现，这是一个有潜力的优化方向——在运行时收集 SMT 求解所需的具体值，引导 Z3 找到反例。

8.2 WASM 运行时的性能

Wasmtime 是 Vera CLI 的默认运行时。它的 JIT 编译（ Cranelift 后端）在大多数场景下性能接近原生代码。

对于性能敏感的代码，vera compile --opt-level=3 启用最高级别优化：

内联小型函数
消除冗余边界检查（已被 SMT 证明安全的情况）
SIMD 向量化

8.3 GC 优化

保守式 GC 的主要开销是 stop-the-world 暂停。Vera 的 GC 实现做了以下优化：

增量 GC：将完整 GC 周期拆分为多个增量步骤
分代假设：新分配对象的死亡率更高，优先扫描年轻代
尾调用优化：递归函数在编译期通过尾调用优化消除栈增长

九、局限性：Vera 不是银弹

客观地说，Vera 也有很多局限性：

9.1 表达力受限

由于强制契约和受限语法，Vera 无法快速编写「先跑起来再说」的脚本代码。相比 Python 的 print("hello")，Vera 需要完整的函数签名和契约。对于需要快速迭代的场景，Python 仍然更合适。

9.2 学习曲线的悖论

虽然 Vera 是为 LLM 设计的，但人类开发者仍然需要理解它——尤其是在调试、审计和交接场景。如果人类无法理解 Vera 代码，整个项目就会陷入困境。

9.3 验证能力有限

Z3 SMT 求解器只能处理它能表达和决策的理论。对于非线性运算、浮点精度、高阶量化等问题，SMT 求解器的表达能力有限，很多场景会降级到 Tier 3 运行时守卫，失去了静态保证。

9.4 生态系统初期

Vera 目前还处于早期阶段（1970 commits），标准库只有 164 个内置函数。相比 Python、JavaScript 成熟的生态，Vera 在库支持方面几乎为零。AI 基础设施库（LLM 调用、向量数据库客户端等）的缺乏是短期内最大的挑战。

十、未来展望：编程语言的新纪元？

Vera 的出现提出了一个更宏大的问题：如果 LLM 真的成为代码的主要编写者，编程语言会走向何方？

我们可以预见几个可能的方向：

方向一：验证型语言的主流化

随着 LLM 能力的提升，「所有代码都可以被验证」不再是一个学术理想，而成为工程实践。Vera 代表了一种极端方向——强验证优先。未来可能出现更多「Vera-inspired」的语言设计，在表达力和验证性之间找到更好的平衡。

方向二：多模型协作的语言抽象

Vera 的效果系统（<Http, Inference>）暗示了一个有趣的可能性：未来的语言可能内置对多模型协作的抽象支持。一个函数调用 LLM，另一个函数调用工具链，第三个函数处理结果——所有效果都在类型层面可见和可验证。

方向三：规格即代码

Vera 的契约本质上是形式化规格说明。这引发了一个更深层的问题：规格语言和实现语言的边界是否会越来越模糊？ 当模型可以在契约和实现之间无缝切换时，「写规格」和「写代码」可能变成同一件事。

方向四：面向 LLM 的语言设计学

Vera 是第一门系统性地针对 LLM 弱点进行设计的语言，但它不会是最后一门。我们可能会看到更多的「LLM 原生」设计：

无歧义语法（LLM 不再混淆相似语法结构）
错误信息即指令（不是给人类诊断，是给模型修复方案）
约束求解集成（SMT/ILP/LP 内置在语法中）
可验证性优先（牺牲表达自由换取可靠性）

结语

Vera 不是一个完美的语言，但它是一个诚实的语言。它承认了一个我们一直在回避的事实：现有的编程语言是为人类设计的，而人类已经不再是代码的主要编写者。

这不是说人类的角色将被取代。恰恰相反——Vera 将人类从「写代码」的苦力活中解放出来，让我们可以专注于定义规范、理解系统、验证结果。契约驱动的开发模式要求我们先想清楚「要什么」，再写「怎么做」，这其实是一种更本质的工程思维。

对于今天的一线工程师来说，Vera 的出现意味着：我们需要重新思考「写代码」这件事的终极目标。如果模型可以写代码，那么我们写代码的真正价值在于：定义什么是正确的，然后让工具去实现它。

拉丁语 veritas（真理）——Vera 的名字本身就是一个宣言。在 LLM 编写代码的时代，真理不在于代码是否「能跑」，而在于代码是否「可证」。

参考资源

Vera GitHub: https://github.com/aallan/vera
官方文档: https://veralang.dev
设计哲学 FAQ: https://github.com/aallan/vera/blob/main/FAQ.md
技术设计文档: https://github.com/aallan/vera/blob/main/DESIGN.md
Z3 SMT 求解器: https://github.com/Z3Prover/z3
Wasmtime: https://github.com/bytecodealliance/wasmtime
实证研究: arXiv:2307.12488 (Models struggle with naming coherence)