# Vera：一种专为机器编写而设计的编程语言

- 来源：Hacker News 热门（buzzing.cc 中文翻译）
- 作者：unignorant
- 发布时间：2026-04-30 21:48
- AIHOT 分数：43
- AIHOT 链接：https://aihot.virxact.com/items/cmolkdy6n00fjslqtz2gvx3u9
- 原文链接：https://github.com/aallan/vera

## AI 摘要

Vera 是一种新型编程语言，专为机器自动编写代码而设计，旨在推动编程自动化。该语言已在 GitHub 平台开源发布，项目地址为 github.com/aallan/vera。自亮相以来，在技术社区 Hacker News 上引发热议，相关帖子获得了 100 点的热度指标，显示出业界对其创新潜力的广泛关注。

## 正文

Vera

Vera (v-ERR-a) is a programming language designed for large language models to write. The name comes from the Latin veritas (truth). Programs compile to WebAssembly and run at the command line or in the browser.

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

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

There are no variable names. @Int.0 is the most recent Int binding; @Int.1 is the one before. The requires clause is a precondition the compiler checks at every call site. The ensures clause is a postcondition the SMT solver proves statically. The function is pure — no side effects of any kind. If any of this is wrong, the code does not compile.

@Int.0

Int

@Int.1

requires

ensures

pure

Why?

Programming languages have always co-evolved with their users. Assembly emerged from hardware constraints. C from operating systems. Python from productivity needs. If models become the primary authors of code, it follows that languages should adapt to that too.

The evidence suggests the biggest problem models face isn't syntax, instead it's coherence over scale. Models struggle with maintaining invariants across a codebase, understanding the ripple effects of changes, and reasoning about state over time. They're pattern matchers optimising for local plausibility, not architects holding the entire system in mind. The empirical literature shows that models are particularly vulnerable to naming-related errors like choosing misleading names, reusing names incorrectly, and losing track of which name refers to which value.

Vera addresses this by making everything explicit and verifiable. The model doesn't need to be right, it needs to be checkable. Names are replaced by structural references. Contracts are mandatory. Effects are typed. Every function is a specification that the compiler can verify against its implementation.

See the FAQ for deeper questions about the design — why no variable names, what gets verified, how Vera compares to Dafny/Lean/Koka/F*, and the empirical evidence behind the design choices.

What Vera looks like

Three examples that show what makes Vera different. For the full tour — contracts, refinement types, ADTs, effects, exception handling, recursion, Markdown, JSON, HTML, HTTP, LLM inference — see EXAMPLES.md.

Contracts the compiler proves

A precondition like requires(@Int.1 != 0) becomes a static obligation: the SMT solver proves it holds at every call site, or refuses to compile. A program that calls safe_divide with a divisor the verifier can't prove non-zero is a compile error, not a runtime error.

requires(@Int.1 != 0)

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 }

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

The verifier checks the contracts the programmer wrote. A function that performs @Int.1 / @Int.0 without a guarding precondition will type-check, verify, and trap at runtime if called with a zero divisor — with a Vera-native diagnostic explaining how to add the missing precondition. Automatically synthesising obligations for primitive operations is the principled long-term move and tracked in #680.

@Int.1 / @Int.0

Effects are explicit

Vera is pure by default. A function that calls an LLM says so in its signature. A caller that doesn't permit cannot invoke it. A caller that doesn't permit cannot invoke it either. Both callers must declare the full effect row.

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

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

Six lines of logic. The signature carries all the ceremony — parameter types, contracts, effect declarations — so the body reads like a pipeline. Run a real example with VERA_ANTHROPIC_API_KEY=sk-ant-... vera run examples/inference.vera. See ENVIRONMENT.md for all VERA_* environment variables (provider keys, runtime knobs, debug flags).

VERA_ANTHROPIC_API_KEY=sk-ant-... vera run

examples/inference.vera

ENVIRONMENT.md

VERA_*

Errors are instructions

Traditional compilers produce diagnostics for humans: expected token '{'. Vera produces instructions for the model that wrote the code. Every error includes what went wrong, why, how to fix it with a concrete code example, and a spec reference.

expected token '{'

[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] 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"

Every diagnostic has a stable error code (E001–E702) and is available as structured JSON via the --json flag.

E001

E702

--json

Getting started

Prerequisites

Python 3.11+

Git

Node.js 22+ (optional, for browser runtime and parity tests)

Installation

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

[dev] includes everything (tests, linters, the language server). For a lighter install that only adds editor/agent support to the base toolchain, use pip install -e ".[lsp]" — see LSP_SERVER.md.

[dev]

pip install -e ".[lsp]"

Tested in CI on every commit:

macOS 15 (Sequoia) and macOS 26 (Tahoe) on Apple Silicon, against Python 3.11, 3.12, 3.13

Ubuntu 24.04 LTS on x86_64, against Python 3.11, 3.12, 3.13

Windows Server 2022 on x86_64, against Python 3.11, 3.12, 3.13

Untested but expected to work (wheels available for all dependencies):

Linux x86_64 with glibc 2.27+ (Ubuntu 18.04+ / Debian 10+ / RHEL 8+)

Linux aarch64 with glibc 2.38+ (Ubuntu 23.10+ / Ubuntu 24.04 LTS / Debian 12+)

macOS 15+ on Intel (x86_64)

Out of scope — pip install -e . will fail at dependency resolution (clear "no matching distribution" error rather than a cryptic source-build failure):

pip install -e .

macOS 14 (Sonoma) and earlier — see #691 for the documented decision and workarounds

Linux aarch64 with glibc ) for IO, etc.

effects(pure)

effects()

Recursive functions need a decreases() clause

decreases()

Match expressions must be exhaustive

Project status

Vera is in active development at v0.0.170 — 1,400+ commits, 171 releases, 4,342 tests, 91% code coverage, 89 conformance programs, 35 examples, and a 13-chapter specification. See HISTORY.md for how the compiler was built.

The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across 13 chapters.

Key features delivered: typed De Bruijn indices (@T.n), mandatory contracts, algebraic effects (IO, Http, State, Exceptions, Async, Inference, Random), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification (Z3 static, guided, runtime fallback), and a language server with warm incremental verification and agent-facing proof-delta methods.

@T.n

What's next: the path from "working language" to "the language agents actually use" — see ROADMAP.md for the four strategic milestones. The flagship goal is a verified MCP tool server where contracts guarantee tool schemas at compile time. VeraBench — a 50-problem benchmark across 5 difficulty tiers — now covers 6 models across 3 providers (v0.0.7). The headline result: Kimi K2.5 achieves 100% run_correct on Vera, beating both Python (86%) and TypeScript (91%). Three models beat TypeScript on Vera; the flagship tier averages 93% Vera vs 93% Python — essentially parity. These are single-run results with high variance — see the full report for details.

Known bugs and open issues are tracked on the issue tracker. See KNOWN_ISSUES.md for a consolidated list.

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 (13 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 │ ├── checker/ # Type checker (mixin package) │ ├── verifier.py # Contract verifier (Z3) │ ├── codegen/ # Code generation (11 modules) │ ├── wasm/ # WASM translation (9 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) + TextMate bundle ├── examples/ # 35 example Vera programs ├── tests/ # Test suite (see TESTING.md) └── scripts/ # CI and validation scripts

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 (13 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 │ ├── checker/ # Type checker (mixin package) │ ├── verifier.py # Contract verifier (Z3) │ ├── codegen/ # Code generation (11 modules) │ ├── wasm/ # WASM translation (9 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) + TextMate bundle ├── examples/ # 35 example Vera programs ├── tests/ # Test suite (see TESTING.md) └── scripts/ # CI and validation scripts

For compiler architecture and internals, see vera/README.md. For testing details, see TESTING.md.

vera/README.md

Design

See DESIGN.md for the full technical decisions table (representation, references, contracts, effects, verification, memory, target, grammar, diagnostics, data types, polymorphism, collections, error handling, recursion, naming) and prior art (Eiffel, Dafny, F*, Koka, Liquid Haskell, Idris, SPARK/Ada, bruijn, TLA+/Alloy).

Contributing

See CONTRIBUTING.md for guidelines on how to contribute to Vera. For compiler internals, see vera/README.md.

Citation

If you use Vera in your research, please cite:

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

Licence

Vera is licensed under the MIT License.

All direct dependencies are MIT or Apache-2.0. One transitive dependency (chardet, via cyclonedx-bom) is LGPL v2+, which is compatible with MIT redistribution. Licence compliance is enforced by CI.

chardet

cyclonedx-bom

Dependency Licence Role Lark MIT LALR(1) parser generator z3-solver MIT SMT solver for contract verification wasmtime Apache-2.0 WebAssembly runtime

Copyright © 2026 Alasdair Allan

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.