Vera

Vera (v-ERR-a) 是一种专为大型语言模型编写而设计的编程语言。其名称源自拉丁语 veritas（真理）。程序编译为 WebAssembly，并可在命令行、浏览器中运行，或——实验性地——在标准 WASI Preview 2 主机上运行。

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 是前一个。requires 子句是编译器在每个调用点检查的前置条件。ensures 子句是 SMT 求解器静态证明的后置条件。该函数是 pure —— 没有任何副作用。如果其中任何一点有误，代码将无法编译。

为什么？

编程语言始终与其用户共同演进。汇编语言源于硬件约束。C 语言源于操作系统。Python 源于生产力需求。如果模型成为代码的主要编写者，那么语言也应随之适应。

证据表明，模型面临的最大问题不是语法，而是规模上的一致性。模型难以在代码库中维护不变量、理解变更的连锁反应以及推理随时间变化的状态。它们是优化局部合理性的模式匹配器，而非将整个系统铭记于心的架构师。实证文献 表明，模型特别容易受到与命名相关的错误影响，例如选择具有误导性的名称、错误地重用名称，以及失去对哪个名称引用哪个值的跟踪。

Vera 通过使一切显式且可验证来解决这一问题。模型不需要正确，它需要可检查。名称被结构引用所取代。契约是强制性的。效应是类型化的。每个函数都是一个规范，编译器可以将其与实现进行验证。

参见 FAQ 以深入了解关于设计的更深层问题——为何没有变量名、验证的内容、Vera 与 Dafny/Lean/Koka/F* 的对比，以及设计选择背后的实证依据。

Vera 的样子

四个示例展示了 Vera 的不同之处。要查看完整指南——契约、精化类型、ADT、效果、异常处理、递归、Markdown、JSON、HTML、HTTP、SQL、LLM 推理——请参见 EXAMPLES.md。

编译器证明的契约

像 requires(@Int.1 != 0) 这样的前置条件成为一个静态义务：SMT 求解器证明它在每个调用点都成立，否则拒绝编译。 一个调用 safe_divide 且除数无法被验证器证明为非零的程序是编译错误，而非运行时错误。

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.1 / @Int.0 现在是编译错误 (E526)，而不是运行时陷阱（对于既不透明又无法翻译的除数，如果既无法证明其非零，也无法见证其为零，则保持 Tier 3，由运行时零除数陷阱保护）；当长度静态已知时，数组索引被证明在界内，当可证明越界时是编译错误 (E527)，否则在运行时进行边界检查；@Nat 减法下溢和 @Int → @Nat 窄化以相同方式检查。 因此，vera verify 报告为已证明的除法或数组索引对所有输入都是安全的；当它无法证明某项时——不透明的除数、动态数组长度，或闭包体内的操作——运行时保护会捕获它，而不是静默地产生错误的值。（浮点除法除外：除以零产生 inf/NaN，而不是陷阱。）

效果是显式的

Vera 默认是纯的。 调用 LLM 的函数会在其签名中说明。 不允许 <Inference> 的调用者无法调用它。 不允许 <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)
  }
}

六行逻辑。签名承载了所有仪式——参数类型、契约、效果声明——因此函数体读起来像一条流水线。使用 VERA_ANTHROPIC_API_KEY=sk-ant-... vera run examples/inference.vera 运行一个真实示例。 参见 ENVIRONMENT.md 获取所有 VERA_* 环境变量（提供商密钥、运行时参数、调试标志）。

SQL 注入无法编译

几乎每个 SQL 注入都以相同的方式开始：一个由来自程序外部的值组装而成的查询。Vera 使这种写法无法实现。DB.query / DB.execute 的 SQL 文本必须写入源代码，因此查询在程序编译时即已固定，外部数据只能通过 ? 占位符和 params 数组到达数据库。

public fn find_user(@String -> @Result<Array<Array<Option<String>>>, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<DB>)
{
  DB.query("SELECT name, email FROM users WHERE name = ?", [Some(@String.0)])
}

用参数来构建查询——string_concat("SELECT ... WHERE name = '", @String.0)——程序将无法编译。E207 将字符串拼接列为注入向量，并给出占位符重写作为修复方案。这不是一个可配置的 lint，也不是一个你运行的污点分析，或一个你记得要指向代码的扫描器：这是一条关于字符串来源的规则，由类型检查器强制执行，因此可注入的形式没有通往可运行程序的路径。试一试：examples/database.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.

  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.2 "Function Declaration Syntax"

每个诊断都有一个稳定的错误代码（E001–E702），并可通过 --json 标志以结构化 JSON 形式获取。

入门

先决条件

• Python 3.11+
• Git
• Node.js 22+ （可选，用于浏览器运行时和一致性测试）

安装

从 PyPI 安装已发布的 veralang 发行版：

python -m venv .venv
source .venv/bin/activate   # Windows: .venv\Scripts\activate
python -m pip install veralang

该发行版命名为 veralang，但已安装的命令仍为 vera，且 Python 代码仍将其导入为 import vera。对于通过语言服务器进行编辑器和代理集成，请安装 python -m pip install "veralang[lsp]"。请勿运行 pip install vera：该 名称属于 PyPI 上一个无关的项目。该 wheel 仅包含编译器和 vera 命令——捆绑的 examples/、一致性测试套件以及 规范位于仓库中，而非 wheel 中。

GitHub 源码途径是代理以及 任何学习该语言的人的推荐环境——它提供了 SKILL.md 所依据的示例、一致性测试程序和 规范，以及工具链——并且 它仍然是编译器开发、未发布更改以及测试当前 main 分支的途径：

git clone https://github.com/aallan/vera.git
cd vera
python -m venv .venv
source .venv/bin/activate   # Windows: .venv\Scripts\activate
python -m pip install -e ".[dev]"

[dev] 包含所有内容（测试、linter、语言服务器）。对于仅为基础工具链添加编辑器/代理支持的更轻量级源码安装，请使用 python -m pip install -e ".[lsp]" — 参见 LSP_SERVER.md。

支持的平台

在每次提交时通过 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
• Ubuntu 24.04 LTS 在 aarch64 上，针对 Python 3.12（建议性任务 — 在每次提交时运行，目前不阻止合并）
• Windows Server 2022 在 x86_64 上，针对 Python 3.11、3.12、3.13

未测试但预期可用（所有依赖项均有可用的 wheels）：

• 带有 glibc 2.27+ 的 Linux x86_64（Ubuntu 18.04+ / Debian 10+ / RHEL 8+）
• 带有 glibc 2.38+ 的 Linux aarch64，在 Python 3.11 / 3.13 上（3.12 单元格已在上述 CI 中测试；例如 Ubuntu 23.10+）
• Intel (x86_64) 上的 macOS 15+

超出范围 — pip install -e . 将在依赖项解析时失败（出现清晰的“no matching distribution”错误，而不是晦涩的源码构建失败）：

• macOS 14 (Sonoma) 及更早版本 — 参见 #691 以了解已记录的决策和变通方法
• 带有 glibc < 2.38 的 Linux aarch64（例如 Ubuntu 22.04 LTS aarch64） — 参见 #701

macOS 15+ 基线反映了 TelemetryDeck 的 macOS 版本分布数据：macOS 26（约 75%）和 macOS 15（约 24%）占 macOS 安装基础的约 99%；macOS 14 约为 1.4% 且正在下降。支持旧版 macOS 版本的成本在该占比下并不划算。

工作流

$ vera check examples/absolute_value.vera
OK: examples/absolute_value.vera

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

$ vera run examples/hello_world.vera
Hello, World!

vera check 进行解析和类型检查。vera verify 通过 Z3 添加契约验证 —— 第一层契约（可判定的算术、比较、布尔逻辑、ADT、终止性）被自动证明；Z3 无法判定的契约成为第三层运行时检查。vera run 编译为 WebAssembly 并执行。

vera run file.vera --fn f -- 42           # call function f with argument 42
vera compile --target browser file.vera   # emit browser bundle
vera compile --target wasi-p2 file.vera   # emit a WASI Preview 2 component (experimental)
vera run --target wasi-p2 file.vera       # execute under the built-in WASI 0.2 host
vera serve file.vera                      # serve handle(Request -> Response) over HTTP (default :8000)
vera compile --target wasi-p2 --world server file.vera  # wasi:http server component for wasmtime serve
vera test file.vera                       # contract-driven testing via Z3 + WASM
vera fmt file.vera                        # format to canonical form
vera verify --json file.vera              # JSON diagnostics for agent feedback loops
vera check --explain-slots file.vera     # show slot resolution table (which @T.n maps to which param)
vera lsp                                 # serve the Language Server Protocol over stdio (see LSP_SERVER.md)
vera version                             # print the installed version
vera builtins --json                     # list the built-in function registry (no file needed)
vera effects --json                      # list the effect and ability registry (no file needed)
vera errors --json                       # list the diagnostic error-code registry E001–E702 (no file needed)

vera compile --target browser 生成一个自包含的捆绑包（wasm + JS 运行时 + HTML），可在任何浏览器中运行——无需构建步骤，无需打包器。强制性的对等测试确保纯语言表面（算术、ADT、模式匹配、闭包、契约、作为宿主导入的效果等）在命令行运行时和浏览器运行时之间具有相同的行为。 IO 表面是文档中记录的例外：依赖 IO.sleep 进行动画节奏控制或依赖 ANSI 转义码进行光标控制的终端 Vera 程序可以干净地编译为 --target browser，但会将转义序列渲染为字面文本，并在休眠期间冻结标签页——浏览器目标期望 Vera 作为纯模拟核心，而由 JavaScript 驱动定时和渲染（SKILL.md §Browser compilation 包含推荐模式）。

vera compile --target wasi-p2 输出一个实验性 WASI Preview 2 目标（IO 和 Random 表面）：一个二进制 WebAssembly 组件，其宿主导入基于 WASI 0.2 接口实现，可由任何标准 wasip2 宿主运行（wasmtime run 无需标志且无需 Vera 绑定）。使用 IO/Random 之外宿主族的程序将被拒绝，并附带指明该族的诊断信息——绝不会静默地针对核心目标进行编译。有关架构、受支持的表面以及已记录的差异（WASI 0.2 的仅 ok/err 退出码，组件边界间无结构化陷阱帧），请参阅 spec 第 13 章。借助 --world server，同一个经过契约验证的 handle(Request -> Response) 程序 vera serve 原生宿主编译为 wasi:http/incoming-handler 组件，标准 wasmtime serve 可未经修改直接运行——作为可移植部署产物的已验证 HTTP 处理器（--world server 仅与 --target wasi-p2 一起有效；CLI 拒绝其他组合）。

编辑器支持

Vera 附带一个 语言服务器（vera lsp，通过可选的 [lsp] 附加组件），它在按键之间保持一个温热的增量 Z3 会话——在编辑器延迟下提供诊断、证明、悬停、槽位跳转定义和类型孔洞补全，以及用于编码代理的自定义证明增量方法。有关设置和完整的协议表面，请参阅 LSP_SERVER.md。

• VS Code 扩展 — 通过 code --install-extension veralang.vera-language 从 Marketplace 安装；自动启动语言服务器，并提供语法高亮和语言配置（来源)
• Vim 软件包 — 适用于 Vim 8+ 和 Neovim 的语法高亮，可作为原生软件包安装或通过插件管理器安装（文件类型为 veralang，而非 vera，后者自 2005 年起被 Vim 用于一种无关的语言）
• TextMate 捆绑包 — 适用于 Sublime Text 及其他 TextMate 语法编辑器的语法高亮（任何具有通用 LSP 客户端的编辑器都可以直接使用 vera lsp）

面向智能体

Vera 为 LLM 智能体提供了以下文件：

• SKILL.md — 完整的语言参考。涵盖语法、槽位引用、契约、效果、常见错误以及可运行的示例。
• AGENTS.md — 适用于任何智能体系统（Copilot、Cursor、Windsurf、自定义）的说明。涵盖编写 Vera 代码以及开发编译器。
• CLAUDE.md — 面向 Claude Code 的项目指南。关键命令、布局、工作流和不变量。
• DE_BRUIJN.md — 深入解析 Vera 的类型化槽位引用：学术背景、实例、交换操作陷阱，以及与证明助手和 LLM 代码生成研究的联系。
• TOOLCHAIN.md — CLI 手册：驱动工具链以编写、验证、测试、运行和调试 Vera，以及 builtins/effects/errors 内省命令。

Claude Code 在此仓库中会自动发现 SKILL.md 和 CLAUDE.md。对于其他项目，请手动安装该技能：

mkdir -p ~/.claude/skills/vera-language
cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md

其他模型 — 在系统提示中、作为文件附件或作为检索文档中包含 SKILL.md。该文件是自包含的，可与任何能够读取 markdown 的模型配合使用。

编写 Vera 代码的基本规则：

1. Every function needs requires(), ensures(), and effects() between the signature and body
2. Use @Type.index to reference bindings — @Int.0 is the most recent Int, @Int.1 is the one before
3. Declare all effects — effects(pure) for pure functions, effects(<IO>) for IO, etc.
4. Recursive functions need a decreases() clause
5. Match expressions must be exhaustive

项目状态

Vera 正处于 v0.1.9 的积极开发阶段：2,000+ 次提交，205 个版本，9,037 个测试，95% 代码覆盖率，179 个一致性程序，42 个示例，以及一份 14 章的规范。已知的缺陷和限制记录在 KNOWN_ISSUES.md。有关编译器构建过程的详细信息，请参阅 HISTORY.md。

参考编译器——解析器、AST、类型检查器、合约验证器（Z3）、WASM 代码生成器、模块系统、浏览器运行时以及运行时合约插入——已可正常工作。语言规范目前处于草稿阶段，涵盖 14 个章节。

已交付的关键特性： 带类型的 De Bruijn 索引 (@T.n)、强制契约、代数效应（IO、Http、HttpServer、State、Exceptions、Async、Inference、DB、Random、Diverge）、精化类型、受限泛型（Eq、Ord、Hash、Show）、代数数据类型、模式匹配、模块、164 个内置函数（字符串、数组、映射、集合、十进制数、数学、JSON、HTML、Markdown、正则表达式、base64、URL）、契约驱动测试、规范格式化器、浏览器运行时、三层验证设计（Z3 静态验证和运行时回退已交付；Z3 引导层已规范定义，尚未实现）、语言服务器 支持热增量验证和面向代理的证明增量方法，以及原生提供（vera serve）或作为 wasi:http 组件为标准 wasmtime serve (--target wasi-p2 --world server) 提供的契约验证 HTTP 处理器。

下一步： 从“可用的语言”到“智能体实际使用的语言”的路径——请参阅 ROADMAP.md 了解四个战略里程碑。旗舰目标是一个经过验证的 MCP 工具服务器，其契约在编译时保证工具模式。 VeraBench ——一个涵盖 5 个难度层级的 60 题基准测试——目前覆盖 3 家提供商的 9 个模型（v0.0.18）。主要结果：九分之六的模型能写出 100% 正确的 Vera，这是一种它们均未接受过训练的语言。在九分之六的模型中，Vera 得分最高或与之持平。该指标为 % solved（pass@1）：拒绝、编译失败、崩溃和错误答案均同等计为未解决。这是首次对全部 60 道题进行评分的测试，因此单道题会使分数变动 1.7 个百分点，且大多数差距仅为一到两道题——详见 完整报告。

已知 bug 和未决问题在 issue tracker 中跟踪。请参阅 KNOWN_ISSUES.md 获取合并列表。

编译器是一个七阶段流水线——请参阅 vera/README.md 深入了解架构：

vera/
├── SKILL.md                       # Language reference for LLM agents
├── AGENTS.md                      # Instructions for any AI agent system
├── CLAUDE.md                      # Project orientation for Claude Code
├── FAQ.md                         # Design rationale and comparisons
├── EXAMPLES.md                    # Language tour with code examples
├── HISTORY.md                     # How the compiler was built
├── ROADMAP.md                     # Forward-looking language roadmap
├── KNOWN_ISSUES.md                # Known bugs and limitations
├── DESIGN.md                      # Technical decisions and prior art
├── TESTING.md                     # Testing reference (single source of truth)
├── CONTRIBUTING.md                # Contributor guidelines
├── CHANGELOG.md                   # Version history
├── LICENSE                        # MIT licence
├── spec/                          # Language specification (14 chapters)
├── vera/                          # Reference compiler (Python)
│   ├── grammar.lark               #   Lark LALR(1) grammar
│   ├── parser.py                  #   Parser module
│   ├── ast.py                     #   Typed AST node definitions
│   ├── transform.py               #   Lark parse tree → AST transformer
│   ├── resolver.py                #   Slot and name resolution
│   ├── checker/                   #   Type checker (mixin package)
│   ├── verifier.py                #   Contract verifier (Z3)
│   ├── codegen/                   #   Code generation (13 modules)
│   ├── wasm/                      #   WASM translation (19 modules)
│   ├── browser/                   #   Browser runtime
│   ├── formatter.py               #   Canonical code formatter
│   ├── errors.py                  #   LLM-oriented diagnostics
│   ├── obligations/               #   Reified proof obligations + warm incremental verification
│   ├── lsp/                       #   Language server (see LSP_SERVER.md)
│   └── cli.py                     #   Command-line interface
├── docs/                          # GitHub Pages site (veralang.dev)
├── editors/                       # VS Code extension (LSP client + grammar), Vim package, TextMate bundle
├── examples/                      # 42 example Vera programs
├── tests/                         # Test suite (see TESTING.md)
└── scripts/                       # CI and validation scripts

有关编译器架构和内部实现，请参阅 vera/README.md。有关测试详情，请参阅 TESTING.md。

设计

有关完整的技术决策表（表示、引用、契约、效果、验证、内存、目标、语法、诊断、数据类型、多态性、集合、错误处理、递归、命名），请参阅 DESIGN.md，以及 prior art（Eiffel、Dafny、F*、Koka、Liquid Haskell、Idris、SPARK/Ada、bruijn、TLA+/Alloy）。

贡献

有关如何为 Vera 做出贡献的指南，请参阅 CONTRIBUTING.md。有关编译器内部实现，请参阅 vera/README.md。

引用

如果您在研究中使用 Vera，请引用：

@software{vera2026,
  author = {Allan, Alasdair},
  title = {Vera: a programming language designed for LLMs to write},
  year = {2026},
  url = {https://github.com/aallan/vera}
}

许可证

Vera 采用 MIT 许可证 授权。

Vera 重新分发的每个依赖项均受与 MIT 兼容的宽松许可证保护。scripts/check_licenses.py 在每次提交和 CI 中对 Python 部分强制执行此规定，并传递性地检查已安装的软件包；VS Code 扩展捆绑的 npm 软件包在此列出，但尚未通过门禁强制执行。

前三个是工具链的运行时依赖项；pygls 和 lsprotocol 随 [lsp] 额外依赖一起提供，编辑器集成需要这些依赖。vscode-languageclient 连同其自身的传递依赖项一起捆绑到 .vsix 中 — vscode-jsonrpc、vscode-languageserver-protocol、vscode-languageserver-types、vscode-languageserver-textdocument 和 brace-expansion（MIT）、semver（ISC）以及 minimatch（BlueOak-1.0.0）。ISC 和 BlueOak-1.0.0 是宽松的，且未施加 MIT 未施加的条件。

版权所有 © 2026 Alasdair Allan

特此授予免费许可，允许任何获得本软件及相关文档文件（“软件”）副本的人，不受限制地处理该软件，包括但不限于使用、复制、修改、合并、发布、分发、再许可和/或销售软件副本的权利，并允许向获得软件的人授予上述权利，但须遵守以下条件：

上述版权声明和本许可声明应包含在软件的所有副本或重要部分中。

软件按“原样”提供，不提供任何形式的明示或暗示保证，包括但不限于对适销性、特定用途适用性和非侵权的保证。在任何情况下，作者或版权持有人均不对因软件或软件的使用或其他交易而产生的任何索赔、损害或其他责任负责，无论是基于合同、侵权或其他原因，均与软件或软件的使用或其他交易有关。