Vera 深度拆解：当编程语言为 AI 原生化而生——一个专为 LLM 打造的零幻觉代码生成范式

前言：当模型成为主要代码作者

2026年，AI 编程助手已经深入到无数工程团队的日常工作流中。从 GitHub Copilot 到 Cursor、Claude Code，AI 生成代码的能力在某些场景下已经可以媲美中级工程师。然而，一个根本性的问题始终没有被认真回答：如果模型成为代码的主要作者，那么语言本身是否应该改变？

Vera（发音 v-ERR-a，来自拉丁语 veritas，意为「真理」）正是对这个问题的一次正面回应。这是一个由 AI 研究者和工程师共同设计的全新编程语言，其核心理念不是「让人类更好地写代码」，而是**「让模型写的代码更容易被验证」**。

本文将深度拆解 Vera 的设计哲学、架构细节、核心特性，并通过大量代码示例展示它如何从根本上解决 LLM 编程的可信度问题。

一、背景：LLM 写代码到底卡在哪里

要理解 Vera 为什么这样设计，先要搞清楚 LLM 写代码时真正的问题是什么。

很多人第一反应是「语法问题」——模型会写错语法、拼错关键字。实际上这是最表层的问题，而且随着模型能力的提升，这个问题已经基本被解决了。

真正的问题有三个：

1.1 命名引发的状态混淆

这是被严重低估的问题。Wang et al. 在论文 "How Does Naming Affect LLMs on Code Analysis Tasks?"（arXiv:2307.12488）中做了系统性的实验：把变量名和函数名替换成乱序或随机字符串，然后测量 CodeBERT 在代码分析任务上的表现变化。

结果出乎意料：打乱的命名（shuffled names）比随机生成的乱码（gibberish）表现更差。这说明什么？当一个变量名叫 count 而另一个叫 result 时，模型会利用这些命名中的统计相关性来做判断，即使任务本身只依赖程序结构。

更严重的是「标识符泄漏」（identifier leakage）现象。Le et al. 在论文 "When Names Disappear"（arXiv:2510.03178）中指出：LLM 在执行预测任务（应该只依赖程序结构）时，也在利用标识符和功能之间的统计关联。模型看起来理解了代码，实际上只是在做模式匹配。

1.2 跨越代码库的推理能力不足

LLM 是上下文窗口优化器。它们擅长在当前上下文中维持一致性，但当代码库规模增大、跨文件依赖变深时，模型很难维护全局不变量。修改一个函数可能导致远处某个地方的假设被打破——而模型看不到这个连锁反应。

1.3 副作用的不可见性

在传统语言中，一个函数声称是「纯函数」但实际上修改了全局状态，这种错误模型很容易犯，也很难被检测出来。Python 的动态类型和隐式副作用使得这个问题更加严重。

二、核心理念：不要让模型做对，而是让模型可被检查

Vera 的设计哲学精髓只有一句话：The model doesn't need to be right, it needs to be checkable.

翻译过来：模型不需要写对，它需要写可以被检查的代码。

这不是降低标准，而是换一个思路解决问题。如果模型的本质是概率生成，那么与其要求它每次都产生正确结果，不如让它产生的每个结果都能被机器自动验证。正确性和可验证性分离——模型负责生成，编译器负责验证。

基于这个理念，Vera 做了三个根本性设计决策：

1. 去掉变量名：用结构化引用替代命名，消除命名歧义
2. 强制契约：每个函数必须有前置条件、后置条件和副作用声明
3. 纯函数优先：副作用必须显式声明，由编译器强制追踪

三、架构解析：编译器如何工作

Vera 的编译器架构分为两层：

3.1 前端：基于类型化 De Bruijn 索引

传统语言用变量名引用绑定：let x = 5; let y = x + 1; // y = 6。模型需要记住 x 指代什么。

Vera 根本不使用变量名，而是用 De Bruijn 索引。每个绑定都有一个位置编号，引用时通过编号访问：

public fn example(@Int -> @Int)
  requires(true)
  ensures(@Int.result >= 0)
  effects(pure)
{
  @Int.0 + 1
}

这里 @Int.0 表示「最近的一个 Int 类型绑定」，@Int.result 表示结果的 Int 绑定。

这个设计彻底消除了命名混淆问题。两个 Int 类型的变量绝不会混淆——它们有各自的位置编号。编译器通过索引解析来验证引用的正确性，不再依赖命名匹配。

学术上 De Bruijn 索引早有先例，但 Vera 在此基础上添加了类型化层：索引不仅记录位置，还记录类型。@Int.0 和 @String.0 是完全不同的引用，无法互换。

3.2 后端：Z3 SMT 求解器做契约验证

每个函数必须声明三个契约：

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

编译器将 requires 和 ensures 翻译为 SMT 可判定的公式片段，交给 Z3 求解。Z3 要么证明条件在所有调用点都成立，要么给出一个反例——此时编译失败，报告具体哪个调用点违反了契约。

这意味着：整数除零不再是运行时错误，而是编译时类型错误。如果你声明 requires(@Int.1 != 0) 且调用方传入了可能为零的值，编译器会直接拒绝，而不是让你的程序在运行时崩溃。

四、核心特性深度解析

4.1 契约验证的三个层次

Vera 的验证分为三层，每层覆盖不同的保证：

第一层：类型系统（机械的、完全的）

类型检查器验证每个引用都解析到正确类型的绑定、每个函数调用匹配签名、每个模式匹配穷尽、泛型正确单态化。这层保证「组件能拼在一起」，是完全可靠的。

第二层：Z3 契约验证（机械的、有界的）

将前置/后置条件翻译为 SMT 公式。当前覆盖：整数和布尔量的线性算术、数组长度、ADT 构造器判别与字段访问、结构递归的终止度量。在当前示例程序中，绝大多数契约都能静态验证——编译器证明实现满足规范，无需运行代码。

对于 Z3 无法判定的部分（涉及泛型类型参数或 closure 体内的符号化状态），fallback 到运行时契约检查——断言仍然执行，只是没有在编译时证明。这些 fallback 是诚实的，不会静默产生错误值。

第三层：代理文档与人类意图（表达的、未验证的）

契约本身是未验证的相对于用户意图——编译器验证契约与实现一致，但不验证契约是否符合你的真实意图。ensures(@Int.result >= 0) 可能完美验证了一个错误的规范。这是 SKILL.md（Vera 的指南规范）存在的意义：引导模型写出意图合理的契约。

4.2 细化类型（Refinement Types）

除了基础的 @Int，Vera 支持细化类型——在类型层面添加约束：

type PosInt = { @Int | @Int.0 > 0 };
type Percentage = { @Int | @Int.0 >= 0 && @Int.0 <= 100 };
type NonEmptyArray = { @Array<Int> | array_length(@Array<Int>.0) > 0 };

PosInt 不是普通的 Int，而是「编译器已证明为正数的整数」。NonEmptyArray 是「编译器已证明非空的数组」。对它们进行索引操作是按构造安全的：

private fn head(@NonEmptyArray -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
{
  @NonEmptyArray.0[0]
}

如果细化类型的约束被违反，编译失败，而不是产生未定义行为。

4.3 代数效应系统（Algebraic Effects）

Vera 默认纯函数。如果一个函数调用 LLM，则必须在签名中声明 <Inference>；如果进行 HTTP 请求，则必须声明 <Http>。调用方如果不许可对应效应，则无法调用该函数：

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)
  }
}

效应传播规则：纯函数调用带副作用的函数时，调用方也必须声明该效应。这使得安全边界的强制执行在类型层面实现——沙箱模块无法执行其声明效应集之外的操作。

4.4 异常作为效应

Vera 将异常建模为代数效应 Exn<E>：

effect Exn<E> {
  op throw(E -> Never);
}

private fn checked_div(@Int, @Int -> @Int)
  requires(true)
  ensures(true)
  effects(<Exn<Int>>)
{
  if @Int.1 == 0 then { throw(0 - 1) } else { @Int.0 / @Int.1 }
}

public fn safe_div(@Int, @Int -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
{
  handle[Exn<Int>] {
    throw(@Int) -> { @Int.0 }
  } in {
    checked_div(@Int.0, @Int.1)
  }
}

safe_div 是纯函数——效应已在 handler 中被消除。调用方无需处理异常，因为 handler 已经将异常转换为返回值。

4.5 内置 Markdown 和 JSON 支持

Vera 为 AI 工作流设计了专门的类型：

public fn main(@Unit -> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  let @Result<MdBlock, String> = md_parse("# Hello\n\n```vera\n42\n```");
  match @Result<MdBlock, String>.0 {
    Ok(@MdBlock) -> {
      if md_has_heading(@MdBlock.0, 1) then {
        IO.print("Has title")
      } else {
        IO.print("No title")
      };
      let @Array<String> = md_extract_code_blocks(@MdBlock.0, "vera");
      IO.print("Code blocks: \(array_length(@Array<String>.0))\n");
      ()
    },
    Err(@String) -> { IO.print(@String.0); () }
  };
  ()
}

JSON 处理同样类型化：

private fn get_name(@String -> @Result<String, String>)
  requires(true)
  ensures(true)
  effects(pure)
{
  match json_parse(@String.0) {
    Err(@String) -> Err(@String.0),
    Ok(@Json) -> match json_get(@Json.0, "name") {
      None -> Err("missing name"),
      Some(@Json) -> match @Json.0 {
        JString(@String) -> Ok(@String.0),
        _ -> Err("name is not a string")
      }
    }
  }
}

模式匹配是穷尽的——如果漏掉某个分支，编译器报错。

4.6 LLM 推理作为效应

Vera 的最激进设计：Inference.complete 直接将 LLM 调用建模为代数效应：

effects(<Inference>)

这使得 LLM 调用变得透明、可组合、可验证。函数的 effects 声明精确列出它可能调用的 LLM 模型，编译器据此追踪依赖关系。

五、实战：从安装到运行

5.1 安装

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

# 如果需要语言服务器（编辑器支持）
python -m pip install "veralang[lsp]"

注意：PyPI 上的包名是 veralang，不是 vera（后者已被其他项目占用）。

5.2 运行第一个程序

创建文件 hello.vera：

effect IO {
  op print(String -> Unit);
}

public fn main(@Unit -> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  IO.print("Hello from Vera!\n");
  ()
}

运行：

vera run hello.vera

5.3 验证（FizzBuzz 示例）

Vera 没有 for 和 while 循环，只有递归：

effect IO {
  op print(String -> Unit);
}

public fn fizzbuzz(@Nat -> @String)
  requires(true)
  ensures(true)
  effects(pure)
{
  if @Nat.0 % 15 == 0 then { "FizzBuzz" }
  else {
    if @Nat.0 % 3 == 0 then { "Fizz" }
    else {
      if @Nat.0 % 5 == 0 then { "Buzz" }
      else { "\(@Nat.0)" }
    }
  }
}

private fn loop(@Nat, @Nat -> @Unit)
  requires(@Nat.0 <= @Nat.1)
  ensures(true)
  effects(<IO>)
{
  IO.print(string_concat(fizzbuzz(@Nat.0), "\n"));
  if @Nat.0 < @Nat.1 then { loop(@Nat.1, @Nat.0 + 1) } else { () }
}

public fn main(@Unit -> @Unit)
  requires(true)
  ensures(true)
  effects(<IO>)
{
  loop(100, 1)
}

注意 fizzbuzz 函数是 effects(pure)——即使内部做了复杂的模运算判断，编译器可以完全用 SMT 验证其行为，无需运行。loop 有 effects(<IO>)，因为它打印输出。两者各司其职，互不污染。

六、与同类语言的对比

6.1 为什么不用 Dafny / Lean / Koka / F*？

这些语言都支持契约验证，但它们是通用语言，语法是为人类设计的。当模型用这些语言写代码时，同样会遇到命名歧义、上下文窗口爆炸、契约与实现不一致等问题。

Vera 的核心创新在于将契约验证与 LLM 编程的工作流整合在一起：错误消息格式化为 LLM 可读的修复指令、内置 Markdown/JSON 类型支持、内置 LLM 推理效应。这些是通用验证语言不会考虑的设计决策。

6.2 为什么不用 Rust？

Rust 的安全保证是通过所有权系统实现的静态保证——但 Rust 最初是为人类程序员设计的，其所有权模型的复杂性本身就对 LLM 构成挑战。模型需要理解借用检查器的全部规则才能写出可编译的代码。

Vera 的契约系统比 Rust 的所有权系统更容易让模型「理解检查规则」：precondition/ensures 是声明性的，Z3 求解是机械的，错误消息格式化为修复指令。而 Rust 的借用检查是隐式的，错误消息往往要求开发者理解整个借用生命周期的推理过程。

6.3 为什么不用 Python / TypeScript？

动态类型语言中，模型可以「猜」类型并运行验证（单元测试），但这依赖于运行时代码执行。Vera 的方法是在编译时做更多工作，减少对运行时测试的依赖。对于 LLM 生成的代码，编译时验证比运行时测试更可靠——因为模型生成的测试用例本身也可能是错的。

七、错误即指令：专为 AI 工作流设计的诊断系统

Vera 最具特色的设计之一是错误消息格式。传统编译器输出诊断信息是为了人类理解：

expected token '{'

Vera 输出的诊断是为写代码的模型准备的指令：

[E001] Error at main.vera, line 14, column 1:

    {
    ^

  Function is missing its contract block. Every function in Vera must declare
  requires(), ensures(), and effects() clauses between the signature and the body.

  Fix:

    Add a contract block after the signature:

      private fn example(@Int -> @Int)
        requires(true)
        ensures(@Int.result >= 0)
        effects(pure)
      {
        ...
      }

  See: Chapter 5, Section 5.2 "Function Declaration Syntax"

每个错误都有稳定的错误代码（E001–E702），且可通过 --json 标志输出结构化 JSON。这使得 CI/CD 管道和 LLM Agent 可以程序化解析和处理错误。

八、生态现状与局限

8.1 当前状态

截至 2026 年 7 月，Vera：

• GitHub 上已有约 1970 次提交
• CI 在 macOS 15/26（Apple Silicon）、Ubuntu 24.04（x86_64 和 aarch64）、Windows Server 2022 上测试通过
• 支持 Python 3.11/3.12/3.13
• 已有 LSP（语言服务器）支持编辑器集成
• 可通过 vera verify --json 进行自动化验证

8.2 当前局限

Vera 仍然是一个早期项目，存在一些明显局限：

1. macOS 14（Sonoma）及更早版本不支持：这意味着在老旧设备上的使用受限
2. 部分 Z3 验证无法覆盖泛型类型参数：泛型函数中的契约在某些情况下只能运行时检查
3. closure/handler体内的部分验证缺失：例如 closure 体内的数组边界目前是运行时检查（Tier 3），不是编译时证明
4. 生态系统早期：缺少大规模库生态，目前主要集中在核心语言特性和工具链

8.3 目标运行环境

Vera 程序编译为 WebAssembly，可以运行在：

• 命令行（通过 Wasmtime 等运行时）
• 浏览器
• 实验性支持标准 WASI Preview 2 主机

这个多目标设计意味着同一份 Vera 代码可以在不同环境中部署，理论上实现了「一次编写，多端运行」的目标。

九、总结：为什么这件事值得关注

Vera 代表了一种全新的编程语言设计思路：不是让人更容易写，而是让机器更容易验证。

传统语言进化的方向是让人类更少地犯错——强类型、借用检查、内存安全——但这些机制最终还是要人类去理解和遵守。Vera 的赌注是：如果完全放手让模型写代码，就应该把验证责任完全交给编译器，而不是期待模型记住所有规则。

这不是说 Vera 会取代任何主流语言。它目前更多是一个实验性项目，目标是验证「LLM-first」语言设计的可行性。但它的设计理念——强制契约、纯函数优先、结构化引用、零幻觉验证——可能会影响未来更多语言的设计方向。

对于今天的工程师来说，Vera 至少提供了三个值得思考的方向：

1. 契约比测试更重要：为 AI 生成的代码写契约，比写单元测试更有价值——因为测试本身也可能被 AI 生成得错误百出
2. 可验证性 > 可读性：当代码的主要读者是 AI 时，设计的优先级应该反转
3. 效应追踪是安全的底线：任何不可追踪的副作用都是潜在的 bug，LLM 编程中尤其如此

如果你是 AI 编程助手的重度用户，或者正在探索 AI Agent 代码生成的工作流，Vera 值得你花时间去了解。即使它最终没有成为主流语言，它提出的问题——「如果模型写代码，语言应该怎么变？」——本身就是 2026 年最值得每个工程师认真思考的技术议题之一。

参考资料

• Vera 官方仓库：https://github.com/aallan/vera
• Vera 官网：https://veralang.dev
• Wang et al., "How Does Naming Affect LLMs on Code Analysis Tasks?", arXiv:2307.12488
• Le et al., "When Names Disappear", arXiv:2510.03178