Vera: 专为 LLM 编写程序设计的编程语言
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, in the browser, or — experimentally — on stock WASI Preview 2 hosts.
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.
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.
Four examples that show what makes Vera different. For the full tour — contracts, refinement types, ADTs, effects, exception handling, recursion, Markdown, JSON, HTML, HTTP, SQL, LLM inference — see EXAMPLES.md.
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.
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 compiler synthesises the same obligations for primitive operations themselves. Computing @Int.1 / @Int.0 where the verifier finds the divisor can be zero is now a compile error (E526), not a runtime trap (an opaque or untranslatable divisor it can neither prove non-zero nor witness a zero for stays Tier 3, guarded at runtime by the zero-divisor trap); an array index is proved in bounds where the length is statically known, a compile error (E527) where provably out of bounds, and otherwise bounds-checked at runtime; @Nat subtraction underflow and @Int → @Nat narrowing are checked the same way. So a division or array index that vera verify reports as proven is safe for all inputs; where it can't prove one — an opaque divisor, a dynamic array length, or an op inside a closure body — the runtime guard catches it rather than silently producing a wrong value. (Float division is exempt: divide-by-zero yields inf/NaN, not a trap.)
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)
}
}
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).
Nearly every SQL injection starts the same way: a query assembled from a value that came from outside the program. Vera makes that unwriteable. The SQL text of DB.query / DB.execute has to be written into the source, so the query is fixed when the program compiles, and outside data can only reach the database through the ? placeholders and the params array.
public fn find_user(@String -> @Result>>, String>)
requires(string_length(@String.0) > 0)
ensures(true)
effects()
{
DB.query("SELECT name, email FROM users WHERE name = ?", [Some(@String.0)])
}
Build the query out of the parameter instead — string_concat("SELECT ... WHERE name = '", @String.0) — and the program does not compile. E207 names string-assembly as the injection vector and gives the placeholder rewrite as the fix. This is not a lint you configure, a taint analysis you run, or a scanner you remember to point at the code: it is a rule about where a string came from, enforced by the type checker, so the injectable form has no path to a running program. Try it: examples/database.vera.
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.
…
Every diagnostic has a stable error code (E001–E702) and is available as structured JSON via the --json flag.
Install the released veralang distribution from PyPI:
python -m venv .venv
source .venv/bin/activate # Windows: .venv\Scripts\activate
python -m pip install veralang
The distribution is named veralang, but the installed command remains
vera, and Python code still imports it as import vera. For editor and agent integration through the language server, install
python -m pip install "veralang[lsp]". Do not run pip install vera: that
name belongs to an unrelated project on PyPI. The wheel ships the compiler and
the vera command only — the bundled examples/, the conformance suite, and
the specification live in the repository, not in the wheel.
The GitHub source route is the recommended environment for agents and for
anyone learning the language — it provides the examples, conformance programs,
and spec that SKILL.md teaches from, alongside the toolchain — and
it remains the route for compiler development, unreleased changes, and testing
the current main branch:
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] includes everything (tests, linters, the language server). For a lighter
source install that only adds editor/agent support to the base toolchain, use
python -m pip install -e ".[lsp]" — see LSP_SERVER.md.
Tested in CI on every commit:
Untested but expected to work (wheels available for all dependencies):
Out of scope — pip install -e . will fail at dependency resolution (clear "no matching distribution" error rather than a cryptic source-build failure):
…
bash mkdir -p ~/.claude/skills/vera-language cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.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 obl
暂无开放 Issues，或尚未同步最近议题。