Vera 编程语言深度解析：当一门语言从设计之初就为 LLM 而生

背景：语言设计的范式转变前夜

2026年的编程世界，正在经历一场静默的革命。

过去六十年，编程语言的设计始终以人类认知为中心：从汇编到C，从Python到Rust，每一门语言都在努力降低人类程序员的认知负担、提升编码效率。我们优化语法糖、改进类型系统、设计更符合直觉的抽象——但这一切的出发点，始终是「人」。

然而，当大模型（LLM）开始在代码生成领域展现出惊人能力时，一个根本性的矛盾浮出水面：人类设计的语言，真的适合 AI 来写吗？

答案是：未必。

2026年5月，一门名为 Vera（发音 v-ERR-a，源自拉丁语 veritas，意为「真理」）的编程语言正式亮相。它的核心主张简单而激进——Vera 不是为人类设计的，它是为 LLM 设计的。从语法结构到类型系统，从错误诊断到验证机制，每一个设计决策都指向同一个目标：让 AI 能够写出正确、可验证、可维护的代码。

这不仅仅是一门新语言，更是一种全新的编程语言设计哲学的宣言。

一、为什么 LLM 写代码的最大问题不是语法

在深入了解 Vera 之前，我们需要先理解一个反直觉的事实：LLM 写代码时，最大的障碍不是语法，而是规模化的语义一致性。

1.1 模型是模式匹配器，不是系统架构师

大量实证研究表明，大型语言模型在代码生成任务中表现出色，尤其在短小、局部、有明确上下文的代码片段上。然而，当代码库规模扩大、需要跨文件维护一致性时，模型的性能会出现显著衰退。

具体来说，LLM 特别容易犯以下几类错误：

命名相关的错误是重灾区。模型会使用误导性的变量名（比如把温度值命名为 user_id），错误地复用已有的命名（在不同作用域中不小心使用了相同名称），以及丢失对「哪个名称指向哪个值」的追踪。这些错误在人类程序员看来是低级的，但在模型生成的代码中却极为普遍。

状态追踪是另一个薄弱环节。模型难以准确追踪跨越多个函数调用的状态变化。当一个值在第23行被修改、随后在第47行被使用时，模型容易产生不一致的更新。

变更的连锁反应最令 LLM 头疼。当修改一个函数签名时，模型需要理解所有调用点是否需要同步更新——这需要「全局视角」，而这恰恰是 Transformer 架构的自注意力机制的边界所在。

1.2 传统语言的「人性化设计」反而成了 AI 的负担

讽刺的是，人类为了降低认知负担而设计的许多语言特性，对 AI 来说反而是负担：

• 变量名是人类理解代码的关键，但也是模型产生命名错误的源头
• 隐式类型转换减少了人类程序员的打字量，但增加了模型推理正确性的难度
• 默认副作用（如可变状态）让人类代码更简洁，但让模型的全局推理更困难
• 宽松的前置条件检查允许运行时才发现错误，但这意味着 AI 无法在编译期就确保正确性

Vera 的设计者意识到：如果模型不需要「被做对」，而是需要「能被检查对不对」，情况会不会完全不同？

这就是 Vera 的核心设计理念。

二、Vera 的核心设计哲学：可验证 > 可读性

Vera 的设计哲学可以浓缩为一句话：「模型不需要写对，它需要写得可以被检查。」

这句话看起来简单，背后却蕴含着一整套语言设计思路的根本性颠覆。

2.1 消灭命名：结构引用替代变量名

在 Vera 中，最具颠覆性的设计是：没有变量名。

不是少用，而是完全不用。看看这段 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.0 指的是最近一个 Int 类型绑定的值，@Int.1 指的是倒数第二个 Int 绑定的值，@Int.result 指的是当前函数的返回值。

这看起来非常反直觉，但背后的逻辑极为精妙：

第一，消除命名歧义。 当模型生成 temp = x + y; result = temp * 2; 时，「temp」这个中间变量名是模型自己发明的，可能与上下文中已有的「temp」冲突，或者含义模糊。而在 Vera 中，结构引用是位置性的，@Int.1 永远指向前一个 Int，不存在歧义。

第二，强制模型表达计算顺序。 因为引用是基于栈式结构的，模型必须显式地组织计算顺序。这减少了「跳过关键步骤」或「隐式依赖某处已有值」这类错误。

第三，便于验证器追踪。 Z3 SMT 求解器在验证合约时，需要精确追踪每一个值的来源和变换。结构引用让这种追踪变得机械化和无歧义。

2.2 强制合约：每函数必须有前置条件和后置条件

Vera 强制要求每个函数声明 requires（前置条件）和 ensures（后置条件）。没有例外。

public fn square_root(@Float -> @Float)
requires(@Float.0 >= 0.0)
ensures(@Float.result >= 0.0)
effects(pure)
{
    // 实现省略
}

这个设计的精妙之处在于：合约是编译器的输入，而不是文档。

在传统语言中，文档注释只是给人看的，编译器完全忽略。但在 Vera 中，合约是编译器必须处理的内容。vera verify 命令会使用 Z3 SMT 求解器来证明：

• 调用点必须满足前置条件，否则编译失败
• 函数体必须实现后置条件，否则验证失败

这意味着，即使模型生成了一个看似合理的函数体，只要前置条件在某个调用点不满足，或者后置条件无法被证明，代码就无法通过编译。

2.3 效果类型：副作用不是隐形的

Vera 默认所有函数都是纯函数（effects(pure)）。如果一个函数要执行 IO、网络请求、调用 LLM 推理，它必须在 effects() 中显式声明：

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

这个设计彻底改变了 LLM 与代码交互的方式：

• 调用方必须声明它允许的副作用集合。如果调用方没有在 effects 中声明 <Inference>，它就无法调用包含 LLM 推理的函数。
• 模型必须正确声明自己函数的效果。如果模型声称某个函数是纯函数但实际上调用了网络请求，验证器会拒绝。
• 整个系统的效果边界变得显式化。这是人类程序员梦寐以求的「显式副作用管理」，对 AI 来说更是防错利器。

2.4 WebAssembly 编译目标：一次编译，处处运行

Vera 编译到 WebAssembly（WASM），可以在命令行和浏览器中无缝运行：

vera run examples/hello_world.vera
# 输出: Hello, World!

vera compile --target browser file.vera
# 生成可在浏览器中运行的 WASM bundle

这种双重运行时的设计，让 Vera 程序天然具备跨平台能力，同时也意味着模型生成的代码可以在沙箱环境中安全执行。

三、技术架构深度解析

3.1 编译器架构

Vera 编译器由以下几个核心组件构成：

Vera 编译器
├── 前端（Python 实现）
│   ├── 词法分析器（Lexer）
│   ├── 语法分析器（Parser）
│   ├── 类型检查器（Type Checker）
│   ├── 合约验证器（Contract Verifier）
│   └── 代码生成器（WASM）
│
├── 后端（Rust 实现，用于 WASM 生成）
│   ├── WASM IR 构建
│   ├── 优化通道
│   └── 二进制编码
│
└── 验证引擎（Z3 SMT 求解器集成）
    ├── Tier 1: 可判定命题（自动证明）
    ├── Tier 2: 需要额外引导的命题
    └── Tier 3: 无法证明，转为运行时检查

Tier 1 验证覆盖：算术运算、比较运算、布尔逻辑、代数数据类型（ADT）、递归终止性证明。这些是 Z3 能够自动处理的范围，模型生成的普通业务逻辑大多落在这个区间。

Tier 3 运行时检查是退路：对于 Z3 无法判定的复杂命题，合约会退化为运行时断言。如果运行时触发未满足的前置条件，程序会报错并给出诊断信息。

3.2 验证器的工作原理

让我们追踪一个具体的验证过程。假设模型生成了以下函数：

public fn absolute_value(@Int -> @Int)
requires(true)
ensures(@Int.result >= 0)
effects(pure)
{
    if @Int.0 < 0 {
        -@Int.0
    } else {
        @Int.0
    }
}

验证器的工作流程：

1. 前置条件检查：在每个调用点，验证器证明 requires(true) 恒成立（直接通过）
2. 后置条件推导：在 if 分支中，结果为 -@Int.0（已知 @Int.0 < 0），所以 -@Int.0 >= 0 成立；在 else 分支中，结果为 @Int.0（已知 @Int.0 >= 0），所以 @Int.0 >= 0 成立
3. Z3 证明：Z3 SMT 求解器接收到上述约束，执行自动证明，两条分支均通过

$ vera verify examples/absolute_value.vera
OK: examples/absolute_value.vera
Verification: 4 verified (Tier 1)

3.3 错误诊断：编译器给模型的「修正指南」

传统编译器产生这样的错误：

Error at main.py, line 14:
    if x = 0:
            ^
SyntaxError: invalid syntax
Did you mean to use '=='?

但 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.

  Vera requires all functions to have explicit contracts so that every function's
  behaviour is mechanically checkable.

  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.1 "Function Structure"

关键差异：

• 包含错误代码（E001-E702）：便于模型精确识别错误类型
• 包含修复代码：直接给出正确实现示例，模型可以复制粘贴
• 包含规范引用：指向语言规范的对应章节
• JSON 输出模式：--json 标志让诊断信息机器可读，适合集成到 Agent 反馈循环中

3.4 工具链完整解析

四、代数数据类型与模式匹配

Vera 支持丰富的代数数据类型（ADT），配合结构化模式匹配：

// 定义代数数据类型
public type Maybe<Int> = None | Some(@Int);

// 使用模式匹配
public fn unwrap_or_default(@Maybe<Int>, @Int -> @Int)
requires(true)
ensures(@Int.result >= @Int.1)
effects(pure)
{
    match @Maybe<Int>.0 {
        None -> @Int.1,
        Some(@Int) -> @Int.1
    }
}

这种设计让模型可以表达复杂的数据结构，同时验证器可以追踪数据流中的每一个值。

五、对比分析：Vera 与相关技术

5.1 与传统合约编程语言的对比

Dafny 和 F* 是非常成熟的验证语言，有着深厚的学术积累。但它们的用户界面是为人类设计的——变量名、文档注释、自然语言规范。Vera 则完全不同，它从零开始思考「如果这个语言的唯一读者是一个 LLM，应该怎么设计」。

5.2 与传统 WebAssembly 语言的对比

5.3 与 AI 原生编程趋势的关系

Vera 的出现并非孤例。2025-2026年，出现了多个「AI 原生」编程语言的探索：

• Swe-agent 系列项目：尝试用特殊 DSL 约束 LLM 的代码生成空间
• TARP（Test-Augmented Repair Projects）：用测试反馈引导 LLM 修正代码
• DSLs for LLM agents：为特定领域设计高度约束的语法，减少 LLM 的搜索空间

Vera 的独特之处在于，它不试图限制 LLM，而是试图使 LLM 的输出可验证。通过将合约变成编译器必须处理的约束，Vera 将 LLM 的「模式匹配」能力与形式化验证的「严格证明」能力结合在一起。

六、生产级实战：从创建项目到完整程序

6.1 环境搭建

Vera 对环境要求相对宽松：

# 克隆仓库
git clone https://github.com/aallan/vera.git
cd vera

# 创建虚拟环境
python -m venv .venv
source .venv/bin/activate

# 安装（含开发工具）
pip install -e ".[dev]"

# 验证安装
vera version

CI 在以下平台测试通过：

• macOS 15 (Sequoia) 和 macOS 26 (Tahoe)，Apple Silicon，Python 3.11/3.12/3.13
• Ubuntu 24.04 LTS，x86_64，Python 3.11/3.12/3.13
• Windows Server 2022，x86_64，Python 3.11/3.12/3.13

6.2 第一个合约验证程序

创建一个阶乘函数，展示合约验证的完整流程：

// factorial.vera

// 基础情况：0! = 1
public fn factorial_base(@Int -> @Int)
requires(@Int.0 == 0)
ensures(@Int.result == 1)
effects(pure)
{
    1
}

// 递归情况：n! = n * (n-1)!
public fn factorial_recursive(@Int -> @Int)
requires(@Int.0 > 0)
ensures(@Int.result == @Int.0 * factorial_of(@Int.0 - 1))
effects(pure)
{
    @Int.0 * factorial_of(@Int.0 - 1)
}

// 包装函数：统一接口
public fn factorial_of(@Int -> @Int)
requires(@Int.0 >= 0)
ensures(@Int.result >= 1)
effects(pure)
{
    if @Int.0 == 0 {
        1
    } else {
        @Int.0 * factorial_of(@Int.0 - 1)
    }
}

// 主函数测试
public fn main(() -> @Int)
requires(true)
ensures(@Int.result == 120)  // 5! = 120
effects(pure)
{
    factorial_of(5)
}

运行验证和执行：

$ vera check factorial.vera
OK: factorial.vera (type checked)

$ vera verify factorial.vera
OK: factorial.vera
Verification: 8 verified (Tier 1)

$ vera run factorial.vera --fn main
120

6.3 调用 LLM 推理：完整的 Agent 程序

Vera 的 Inference 效果让程序可以原生调用 LLM。以下是一个完整的 AI 辅助研究工具：

// research_agent.vera

public type SearchResult = Ok(@String) | Err(@String);

// 带合约的 HTTP 请求
public fn fetch_page(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Http>)
{
    Http.get(@String.0)
}

// 调用 LLM 进行摘要
public fn summarise(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Inference>)
{
    Inference.complete(
        string_concat("Summarise this in 3 bullet points:\n\n", @String.0))
}

// 完整研究流程
public fn research(@String -> @Result<String, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects(<Http, Inference>)
{
    let @String query = @String.0;
    
    // 第一步：获取搜索结果
    let @Result<String, String> page = Http.get(
        string_concat("https://api.example.com/search?q=", query));
    
    match page.0 {
        Ok(@String) -> {
            // 第二步：LLM 摘要
            summarise(@String.0)
        },
        Err(@String) -> Err(
            string_concat("Search failed: ", @String.0))
    }
}

使用环境变量配置 API Key：

export VERA_ANTHROPIC_API_KEY=sk-ant-...
vera run research_agent.vera --fn research -- "最新 Rust 生态进展"

6.4 浏览器端运行

将同样的代码编译为浏览器可执行文件：

vera compile --target browser research_agent.vera
# 生成：research_agent_bg.wasm + research_agent.js + index.html

生成的 HTML 包含完整的 WASM 运行时，可直接在浏览器中运行，无需任何构建步骤或打包工具。

七、LLM 友好设计的高级话题

7.1 Slot 解析：@T.n 的语义规则

Vera 的结构引用系统有一套精确的语义规则，--explain-slots 标志可以展示完整的引用映射表：

$ vera check --explain-slots examples/advanced.vera

Slot Resolution Table for advanced.vera:
@Int.0  → 第一个 Int 参数 (line 5)
@Int.1  → 第二个 Int 参数 (line 5)  
@Int.2  → let 绑定 (line 12)
@Int.3  → 递归调用返回值 (line 15)
@Int.result → 函数返回值 (line 18)

这个映射表对 LLM 来说极为有价值——它让模型能够理解自己生成的引用，而不必依赖猜测或记忆。

7.2 多层函数的作用域追踪

当函数嵌套调用时，结构引用的栈式语义自然地处理了作用域问题：

// 外层函数
public fn outer(@Int, @Int -> @Int)
requires(@Int.0 >= 0 and @Int.1 >= 0)
ensures(@Int.result >= 0)
effects(pure)
{
    // @Int.0, @Int.1 来自外层
    
    let @Int inner_result = inner_helper(@Int.0);
    // @Int.inner_result 现在是栈顶 Int
    
    @Int.0 + @Int.inner_result
    // @Int.0 在 let 之后仍然可用
}

// 内层助手函数
private fn inner_helper(@Int -> @Int)
requires(@Int.0 >= 0)
ensures(@Int.result >= @Int.0)
effects(pure)
{
    @Int.0 * 2
}

7.3 效果行类型系统

Vera 的效果系统采用了行类型（Row Types）的思想：

// 函数可以请求任意效果集
public fn maybe_http(@Bool -> @Result<String, String>)
requires(true)
ensures(true)
effects(<Http>)
{
    if @Bool.0 {
        Http.get("https://example.com")
    } else {
        Ok("Skipped")
    }
}

// 调用方必须声明其效果预算
public fn caller(() -> @Result<String, String>)
requires(true)
ensures(true)
effects(<Http>)
{
    maybe_http(true)
}

如果 caller 没有声明 <Http> 效果，effects(pure) 会导致编译错误。这种强制效果声明确保了效果的可见性——任何调用链上的副作用都必须在根调用点可见。

八、当前局限性与未来方向

8.1 已知的局限性

运行时退化（Tier 3）：Z3 无法判定的复杂命题会退化为运行时检查。这意味着某些合约只能在运行时验证，而非编译时证明。这对于 LLM 生成的安全性是一个缺口。

递归终止性：验证器对递归函数有终止性检查，但如果模型生成无穷递归，验证器可能无法在合理时间内给出结论。Issue #680 正在追踪这个问题——目标是自动为原始操作合成验证义务。

命名缺失的认知负担：对于人类程序员来说，无变量名的代码可读性极低。虽然这对于 LLM 是优势，但对于需要 debug 或 review 人类参与的场景（目前还很常见），这是显著的缺点。

标准库尚在完善：截至 2026 年 5 月，Vera 的标准库覆盖范围有限，许多常见操作（如复杂字符串处理、文件系统操作）需要通过效果系统从宿主环境导入。

8.2 未来路线图

从 GitHub 仓库的 open issues 和里程碑来看，以下方向值得关注：

• Tier 1 覆盖率扩展：逐步将更多合约义务纳入自动证明范围，减少 Tier 3 运行时退化
• 更多编译目标：除了 WASM，探索编译到原生代码和 JavaScript 的可能性
• 标准库丰富：为 HTTP、JSON、文件系统等常见场景提供经过验证的标准库函数
• LLM 训练数据优化：Vera 的 GitHub 仓库（1346 commits）已积累了丰富的正确程序，这些代码可以作为训练数据，专门优化 LLM 生成 Vera 代码的能力

8.3 对 AI 编程工具链的启示

Vera 的出现，对整个 AI 编程工具链都有深远的启示：

第一，「生成 + 验证」循环比「生成 + 测试」更高效。 传统流程是 LLM 生成代码 → 人类写测试 → 运行测试发现问题。Vera 的合约系统让编译器在生成阶段就介入验证，将错误发现提前了数个环节。

第二，领域特定约束可以显著提升 AI 生成质量。 通过强制合约声明和效果类型，Vera 将 LLM 的「自由发挥空间」约束在一个更容易正确的子空间。这比用通用语言 + 人工 code review 的方式更高效。

第三，编译器的错误信息设计需要重新思考。 当编译器的主要读者是 AI 时，诊断信息的格式和内容都需要重新设计——不仅要知道「哪里错了」，更需要知道「怎么改」和「为什么错」。

九、总结与展望

Vera 不仅仅是一门新语言，它是 2026 年编程语言设计领域最具思想性的实验之一。

它的核心洞察是：LLM 写代码的最大问题不是能力不足，而是缺乏一种能够约束其输出、使其输出可验证的语言。通过消灭变量名（消除命名歧义）、强制合约声明（使行为可验证）、显式效果类型（使副作用可见），Vera 为 LLM 代码生成提供了一个全新的技术基座。

从技术实现上看，Vera 融合了形式化验证（Z3 SMT）、现代类型系统（代数数据类型 + 效果行类型）、以及 WebAssembly 编译目标，这些成熟技术的组合产生了意想不到的化学反应。

从哲学上看，Vera 代表了一种逆向思维：与其要求 AI 学习人类的语言，不如为 AI 设计一门适合它的语言。这个转变的深远影响，可能超出编程语言本身——它暗示了未来 AI 与软件工程交互的全新范式。

如果你正在构建 AI 编程 Agent、Vibe Coding 工作流、或者形式化验证工具，Vera 值得你投入时间去研究。它的 1346 commits 和活跃的社区表明，这不是一个学术玩具，而是一个正在快速发展的生产级项目。

语言的名字是 veritas——真理。在 LLM 生成代码越来越普及的时代，「真理」意味着「可以被证明正确的代码」。这或许正是未来编程语言进化的方向。

参考资料：

• Vera 官方仓库：https://github.com/aallan/vera
• Vera 官网：https://veralang.dev
• Z3 SMT 求解器：https://github.com/Z3Prover/z3
• WebAssembly 官方规范：https://webassembly.org/