The short answer is that variable names are one of the things that confuses LLMs rather than helps them. Unlike with humans, names undermine a model's efforts to keep track of state over larger scales. Models confuse similarly named variables in different parts of the codebase easily. Names help us; they don't help them.
The longer answer is more interesting. Wang et al. ("How Does Naming Affect LLMs on Code Analysis Tasks?", arXiv:2307.12488) systematically replaced variable and function names with nonsense or shuffled strings and measured the impact on CodeBERT across code analysis tasks. Good names do help LLM performance — but shuffled names (where a variable named count gets swapped with one named result) perform worse than random gibberish. The model actively gets misled by plausible-but-wrong names. Python, being dynamically typed, is hit harder than Java, because models compensate for lost names using type declarations in statically typed languages.
That last point is the Vera thesis in miniature. In a language with strong types, explicit contracts, and no variable names, the model can't fall back on the naming crutch, but it also can't be misled by it. It has to use the structural information.
Le et al. ("When Names Disappear", arXiv:2510.03178) make this sharper still: LLMs exploit statistical correlations between identifiers and functionality even on execution prediction tasks that should depend only on program structure. They call this "identifier leakage." The model appears to understand code when it's actually pattern-matching on familiar tokens.
So the problem isn't that variable names are useless to LLMs. It's that they're a crutch that lets the model appear to understand code when it's actually not reasoning about the code. Vera's bet is that if you remove the crutch and give the model verified structural information instead — contracts, types, effect declarations — you force it onto firmer ground.
See DE_BRUIJN.md for a deeper treatment: where the indexing idea comes from academically, how Vera's typed variant differs from classic De Bruijn indices, worked examples of the common traps (particularly the commutative-operations pitfall), and further reading.
You could absolutely build a bidirectional transform: names in, indices out for the model, indices back to names for humans. The tooling for that would be straightforward.
The reason Vera doesn't do this is that the canonical form is the language. If names exist in the source, they're part of the program, which means they can diverge from intent, be inconsistent, or be misleading — and now you have two representations to keep in sync. Vera sidesteps that by having one representation that's unambiguous by construction. The model writes exactly what the compiler sees. No translation layer, no sync problem.
That said, a visualiser that infers human-readable names from types and usage for display purposes is interesting tooling on top of Vera. The canonical form stays clean for the model, but humans get an annotated view when they need one.
This is a fair point. The contracts can say what the output cannot be, but if the constraints fully determine the output then the function body is superfluous. So the implementation matters, and shouldn't the implementation be tied to the human's requirements?
Vera's answer is that the contracts are the link between implementation and requirements. The human writes (or reviews) the contracts — preconditions, postconditions, effect declarations — and those are small, declarative, and human-readable. The compiler then proves the implementation satisfies them. The human audits the specification, not the code.
The bet is that contracts are a better surface for capturing intent than variable names scattered through an implementation. A function signature with requires(@Int.1 != 0) and ensures(@Int.result == @Int.0 / @Int.1) communicates what the function does more precisely than any variable name could.
There are three layers, and they cover different things.
Layer 1: Type system (mechanical, complete). Every binding uses typed De Bruijn indices (@Int.0, @String.1, etc.), so the type checker can verify that every reference resolves to a binding of the correct type, every function call matches its signature, every pattern match is exhaustive, and generics monomorphise correctly. This is the "components slot together" layer. Nothing novel here beyond the index scheme, but it's total — if it type-checks, the pieces fit.
Layer 2: Z3 contract verification (mechanical, bounded). Every function has mandatory preconditions, postconditions, and effect declarations. The compiler translates these into a decidable SMT fragment and hands them to Z3. Currently that fragment covers linear arithmetic over integers and booleans, array lengths, ADT constructor discrimination and field access (via Z3 datatype sorts), and termination measures for structural recursion. Across the current example programs, the vast majority of contracts verify statically — the compiler can prove the implementation satisfies the spec without running the code. The remainder are contracts involving generic type parameters (a fundamental SMT limitation) or symbolic effect state modelling across handlers. These fall back to runtime contract checking: the assertions still execute, they just aren't proven at compile time.
This layer does cover actual correctness properties, not just interface compatibility. If you write ensures(@Nat.result >= 0) on an absolute value function, the compiler will either prove it holds for all inputs or give you a counterexample.
Layer 3: Agent documentation and human intent (expressive, unverified). The contracts themselves are unverified with respect to user intent. Nothing in the pipeline checks whether ensures(@Int.result >= 0) is actually what you wanted the function to do. The contract could be a perfectly verified implementation of the wrong specification. This is where SKILL.md lives — it steers the model toward writing contracts that capture reasonable intent, but "reasonable" has no formal backing.
So: provably correct relative to stated requirements, yes. Provably correct relative to unstated intent, no — but the auditable surface is deliberately as small as possible. The human reviews contracts, not implementations.
Yes. 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 argument of DB.query / DB.execute must have literal provenance. It can be a string literal, or a string_concat, an interpolation, or a let chain — but every part of that chain has to trace back to a literal. A query built from a parameter, a call result, or a \(expr) interpolation of one is rejected at compile time with E207. Data from outside the program reaches the database only through the ? placeholders and the params array:
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)])
}
Swap the placeholder for string_concat("SELECT ... WHERE name = '", @String.0) and the program does not compile.
That is worth separating from the protections you are probably used to. It is not a lint, so there is no configuration to get right and no suppression comment to add. It is not a scanner run over a build, so it cannot be skipped or fall behind the code. And it is not a solver result, so it does not weaken where the solver does: Vera's contract verification has tiers and can fall back to runtime checks, but this check has neither. It asks one question about where a string came from, answers it in the type checker, and gives the same answer inside handled code and generic code as anywhere else.
Two smaller errors sit alongside it. A ?-placeholder/parameter count mismatch is E208 when the params array's length is statically known — written out at the call site, or reached through a let — while anything else defers that arity check to the driver — and numbered or named placeholder styles are rejected in favour of the single positional form (E209).
The guarantee is exactly as wide as the query path, and no wider. Every string that reaches the database goes through DB.query / DB.execute, and the language has no other string-to-SQL route, so there is no back door to leave open. What it does not catch is a fixed query that is simply wrong: a literal DELETE FROM users compiles happily, because nothing in it came from outside. And in v1 the effect is SQLite-only and un-mockable (handle[DB] is tracked with the other host effects in #372; further backends are #1143).
It does — the verifier auto-synthesises a proof obligation at every primitive operation whose well-definedness depends on operand values, and discharges it from the surrounding preconditions and path conditions. Integer division and modulo by zero carry a b != 0 obligation (E526) — float division is exempt, since f64.div by zero yields inf or NaN rather than trapping; array indexing carries a 0 <= i < array_length(arr) obligation (E527); @Nat subtraction underflow and @Int → @Nat narrowing carry >= / >= 0 obligations (E502 / E503). A function that declares requires(@Int.1 != 0) and performs @Int.0 / @Int.1 is statically proven non-trapping; a function that declares requires(true) and performs @Int.1 / @Int.0 is now a compile error (E526), not a silent runtime trap. (An operation inside a closure body, quantifier predicate, or handler clause is walked under a fresh slot scope: a slot-dependent obligation is reported as a Tier-3 entry — runtime-guarded at the codegen-guarded sites, while the documented unguarded sites (a user effect-operation argument or generic-instantiated constructor field, disclosed as tier3_unguarded/E504, and a refined nested constructor sub-pattern, disclosed as tier3_unguarded/E506) carry no codegen guard and say so in the stream — while a manifest violation like 5 / 0 is the same loud compile error as direct position. A quantifier domain and a handler's state-init and body are enclosing-scope positions and prove at full precision.)
You discharge an obligation by encoding the constraint in a precondition (requires(...)), a guarding if (whose path condition holds in the relevant branch), or a refinement type ({ @Int | @Int.0 != 0 }) — the verifier then proves it at every call site. Integer division and modulo are decidable, so an unguarded divisor the solver can show may be zero is a compile error (E526); a divisor the solver can't translate — opaque, like a value behind an uninterpreted call — falls to a Tier-3 runtime guard instead, the same way array bounds do. Array bounds depend on array_length, which the solver treats as opaque, so they are proven at Tier 1 only where a literal length, refinement, precondition, or path condition pins it — and a provably out-of-range index (e.g. [1, 2, 3][5]) is a compile error (E527).
Where a bound can't be proved at Tier 1 — a dynamic array index whose length the solver can't pin, or an index inside a closure body — it falls to a runtime-guarded Tier 3 rather than a static proof, and that fallback is honest, not silent: vera verify --json counts it. Those traps are Vera-native — each carries a kind label (divide_by_zero, out_of_bounds), a per-kind Fix: paragraph naming the precondition that would lift it to a static proof, and a source backtrace.
These obligations are auto-synthesised as of #680. Lifting dynamic or closure-captured array bounds from a runtime-guarded Tier 3 to a Tier-1 proof is part of the Tier 2 verification work (#427).
Every function in Vera must declare what it requires, what it guarantees, and what side effects it performs. The compiler proves the implementation satisfies those contracts via Z3 — it either verifies statically or gives you a counterexample. So a compliance reviewer can audit the contracts (which are small and declarative) without reading the implementation, and the compiler proves the code matches them.
The effect system adds another dimension: a function that declares effects(pure) is proven to have no side effects. A function that declares effects(<IO>) can only perform IO operations. A caller that only permits <Http> cannot invoke a function that also performs <IO>. This makes it possible to enforce security boundaries at the type level — a sandboxed module literally cannot perform operations outside its declared effect set.
Abilities are Vera's mechanism for constrained generics — type constraints that restrict what types a generic function can accept. They're inspired by Roc's ability system and serve a similar role to Haskell's type classes or Rust's traits, but with a fixed set of built-in abilities rather than user-defined ones.
Vera has four built-in abilities:
Eq<T>— equality comparison viaeq(a, b), satisfied by all primitive types and ADTs whose fields are themselvesEqOrd<T>— ordering viacompare(a, b), which returns the built-inOrderingADT (Less,Equal,Greater), satisfied byInt,Nat,Bool,Float64,String, andByteHash<T>— hashing viahash(x), which returns anInt, satisfied byInt,Nat,Bool,Float64,String, andByteShow<T>— string conversion viashow(x), satisfied byInt,Nat,Bool,Float64,String, andByte
You use them in generic signatures with where clauses:
public forall<T where Eq<T>> fn contains(@Array<T>, @T -> @Bool)
requires(true)
ensures(true)
effects(pure)
{
...
}
The compiler checks at every call site that the concrete type satisfies the required ability. ADTs can auto-derive Eq if all their constructor fields are themselves Eq-satisfying types — simple enums satisfy Eq automatically.
The design choice to fix the ability set (rather than allowing user-defined abilities) is deliberate: it keeps the language simpler for models and avoids the coherence problems that plague open type class systems.
HTTP is modelled as a built-in algebraic effect. Http.get(url) and Http.post(url, body) are effect operations that return Result<String, String>. Functions that use them must declare effects(<Http>) in their signature, making network access explicit and trackable in the type system.
The effect system means a caller that only permits <IO> cannot invoke a function that performs <Http> — network access is a separate capability. In tests, you can provide mock handlers instead of making real network requests. The pattern for fetching and parsing JSON from an API is: call Http.get, then json_parse the response body.
Currently HTTP supports GET and POST. Custom headers, additional HTTP methods, response status codes, timeouts, and streaming are tracked as known limitations (#351–#356).
Yes. vera compile --target browser produces a self-contained directory with a .wasm binary, a JavaScript runtime (runtime.mjs), and an index.html:
vera compile --target browser examples/hello_world.vera
# produces examples/hello_world_browser/
# module.wasm
# runtime.mjs
# index.htmlServe it with any HTTP server and open index.html — no build step, no bundler, no dependencies. The JavaScript runtime provides browser-appropriate implementations of all Vera host bindings: IO.print writes to the page, IO.read_line uses prompt(), and all other operations (State, contracts, Markdown) work identically to the wasmtime runtime.
The runtime also works in Node.js:
node --experimental-wasm-exnref vera/browser/harness.mjs module.wasmMandatory parity tests enforce that the browser runtime produces identical results to the wasmtime runtime on every PR.
vera test is Vera's built-in testing command. It generates test inputs automatically from function contracts — you don't write test cases manually.
The process works in three steps:
-
Input generation: The compiler reads each function's
requires()clause and uses Z3 to generate concrete values that satisfy the precondition. For example, if a function requires@Int.1 != 0, Z3 produces pairs of integers where the second is non-zero. It generates up to 100 trials per function by default (configurable with--trials). -
Execution: Each generated input is compiled to WASM and executed via wasmtime. The function runs with real values, not symbolic ones.
-
Contract checking: The
ensures()postcondition is checked against the actual output. If any trial produces a result that violates the postcondition, the test fails with the concrete input that triggered it.
vera test examples/safe_divide.vera # test all functions
vera test --trials 50 examples/safe_divide.vera # limit trials
vera test --json examples/safe_divide.vera # JSON output for agentsThis combines the best of property-based testing (generated inputs, no manual cases) with the best of formal verification (inputs derived from specifications, not random). The contracts serve double duty: they're both the specification the compiler proves and the test oracle that validates runtime behaviour.
The reference compiler targets WebAssembly, so the initial applications are web-based. The .wasm binary runs at the command line via wasmtime or in any browser with the self-contained JavaScript runtime.
But the deeper answer is that the end users aren't humans directly — they're AI coding agents. The intended workflow is: a human (or an orchestrating agent) describes what they want; a model generates Vera code; the compiler verifies it; the WASM binary runs. The human's job is to review contracts, not implementations.
HTTP, JSON, and Markdown are now built-in, which supports the primary agent workloads: API integration, data processing, and structured document generation. A Vera program can make an HTTP request, parse the JSON response, and return typed, contract-checked data — all with the network I/O declared as an algebraic effect (effects(<Http>)). A research function that fetches data from the web, processes results via LLM inference, and returns typed, contract-checked Markdown output is the kind of program Vera is designed for.
Vera-specific benchmark data is now available across multiple models. VeraBench — a 60-problem benchmark across 5 difficulty tiers — covers 9 models across 3 providers (v0.0.18). The headline result: six of the nine write 100% correct Vera, a language none of them was trained on. Vera has the highest score, or level with it, for six of the nine models. The metric is % solved (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved, so a model cannot score higher by answering less.
The sharpest evidence that the design choices are doing the work is Vera against Aver, a second language that is also absent from every training set and also learned from a single document in the prompt — so familiarity cannot explain a difference between them. What separates them is that Aver has ordinary variable names where Vera has typed slot references. Vera scores higher on all five models that ran both. The two languages differ in more than one respect, so this isolates the variable better than the Python comparison without isolating it completely.
These caveats matter: single run per model, no pass@k. v0.0.18 is the first sweep in which all 60 problems are graded, so one problem is worth 1.7 percentage points — which narrows the increment but does not remove the caveat, since most of the gaps are still one or two problems wide. Stable rates will require pass@k evaluation with multiple trials — see the full report for details.
The broader literature is also encouraging. The type-constrained decoding paper (Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025, ACM DL) found that enforcing type constraints during LLM code generation cut compilation errors by more than half and improved functional correctness by 3.5–4.5%. Syntax constraints alone provided limited improvement — it was the type constraints that made the difference. The same paper found that 94% of LLM-generated compilation errors are type-check failures — exactly the class of error that a strong static type system catches at compile time.
The Vericoding benchmark (Sun et al., "A Benchmark for Vericoding", arXiv:2509.22908) shows LLMs achieving 82% verification success on Dafny versus 27% on Lean, which suggests SMT-automated verification (Vera's approach) is significantly more LLM-tractable than explicit proof construction.
Blinn et al. ("Statically Contextualizing Large Language Models with Typed Holes", OOPSLA 2024, ACM DL) demonstrated that providing type context at incomplete program locations significantly improves LLM completion quality — a result that directly motivates Vera's planned typed holes feature (#226).
None of this is Vera-specific, but it validates the design choices. The thesis is plausible, the tooling exists, and initial Vera-specific results are consistent with the broader literature. What's needed is expanded and replicated evaluations — more models, more tiers, and longitudinal tracking across releases — to confirm these findings across languages and settings.
This is a real concern. LLMs are trained on trillions of tokens of Python, TypeScript, and JavaScript. A MojoBench study (NAACL 2025) found that even fine-tuned models achieved only 30–35% improvement over base models on Mojo code generation, illustrating the cold-start problem for new languages.
Vera's approach has three parts. First, the agent-facing documentation (SKILL.md) is designed to be dropped into a model's context window, so the model works from the language specification rather than training data recall. Second, Vera's syntax is deliberately simple and regular — fewer constructs, each with exactly one canonical form — which reduces the surface area a model needs to learn. Third, the conformance test suite (179 programs covering every language feature) gives models concrete examples to learn from and conform to. Simon Willison's December 2025 JustHTML write-up illustrates the same point in practice: an LLM-assisted implementation, guided by the html5lib conformance suite, conformed to the HTML parsing spec by running against its tests — a comprehensive test suite is a strong scaffold for a model implementing to a specification.
Dafny shares Vera's Z3/SMT verification approach and is used in production at AWS (Cedar authorisation). But it's imperative, lacks algebraic effects, and has optional (not mandatory) annotations. The 2025 paper proposing Dafny as a verification intermediate language for LLM-generated code validates Vera's core thesis — but Dafny wasn't purpose-built for it.
Lean 4 has the richest LLM integration ecosystem (LeanDojo, Lean Copilot) and significant investment. But it's primarily a theorem prover with monadic effects. LLMs achieve only 27% success rate on Lean versus 82% on Dafny, suggesting explicit proof construction is harder for models than SMT-automated verification.
Koka pioneered the row-polymorphic algebraic effect type system that Vera draws from. But it has no verification, no contracts, and isn't production-ready.
F* combines refinement types, algebraic effects, and SMT-based verification. It's the closest to Vera's feature set, but targets human programmers, not models. It also has a steep learning curve.
No production language today combines mandatory contracts, algebraic effects, refinement types, constrained generics with built-in abilities, De Bruijn indices, Z3 verification, and WebAssembly compilation into a single design optimised for LLM code generation.
Three reasons. First, portability — the same .wasm binary runs at the command line or in any browser. Second, sandboxing — WebAssembly has no ambient capabilities, so a Vera program cannot do anything its effect declarations don't permit. Third, the WASM Component Model (W3C, production-ready in Wasmtime) will enable Vera components to interoperate with Rust, Go, and Python components via WIT interfaces, providing ecosystem access without requiring a massive native package system.
Correctness over performance. The reference compiler is a specification-faithful implementation, not a production compiler. Python makes the compiler readable, testable, and easy to modify during rapid language evolution. The seven-stage pipeline (parse → transform → resolve → typecheck → verify → compile → execute) is independently testable at each stage.
If Vera reaches the point where compiler performance matters, a production compiler in Rust or OCaml would be a separate project. The Python reference compiler would remain as the specification oracle.
Because the whole point is that code should be checkable. If contracts are optional, models won't write them — and then you're back to unverifiable code. Making contracts mandatory means every function is a specification that the compiler can verify against its implementation. The model doesn't need to be right; it needs to be checkable.
This is a deliberate trade-off. Mandatory contracts add friction. But the friction is the feature — it forces the model (and any human) to state what the function requires, what it guarantees, and what effects it performs. That statement is the auditable surface.
The reference compiler is under active development. The current release includes:
- A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
- A 14-chapter formal specification
- 9,037 tests, including a 179-program conformance suite
- 42 working example programs
- 164 built-in functions covering strings, arrays, math, parsing, and data types
- Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation
- Full IO operations (print, read_line, read_char, read_file, write_file, args, exit, get_env, sleep, time, stderr)
- Algebraic data types, pattern matching, closures, generics with monomorphisation
- Algebraic effect handlers with resume and state
- Built-in
<Http>,<HttpServer>,<Inference>,<DB>,<State>,<IO>,<Async>,<Random>,<Diverge>, andExn<T>(typed exception) effects <Inference>dispatches to Anthropic, OpenAI, Kimi (Moonshot), or Mistral via env vars- Collection types:
Map<K,V>,Set<T>,Array<T>,Decimal,Json,HtmlNode,Markdown - String interpolation with auto-conversion for primitive types
- Cross-module imports with contract verification at call sites
- Contract-driven testing via Z3 and WASM
- A canonical code formatter
- WebAssembly compilation and execution via wasmtime
- Browser runtime with mandatory parity tests
The language is under active development. See the Roadmap and Changelog for current status and planned features.
Clone the repository — the checkout carries the bundled examples this command runs, plus the conformance suite and specification (a PyPI install ships the toolchain only):
git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && source .venv/bin/activate
python -m pip install -e .
vera run examples/hello_world.veraIf you only need the vera command — no examples, spec, or conformance programs — install the released distribution from PyPI:
python -m venv .venv && source .venv/bin/activate
python -m pip install veralang
vera versionFor agents, point your model at SKILL.md. It's the complete language reference, designed to be dropped into a context window. For driving the command-line toolchain itself — checking, verifying, testing, running, and debugging Vera, plus the builtins/effects/errors introspection commands — see the CLI cookbook, TOOLCHAIN.md.
- Wang et al., "How Does Naming Affect LLMs on Code Analysis Tasks?", arXiv:2307.12488
- Le et al., "When Names Disappear: Revealing What LLMs Actually Understand About Code", arXiv:2510.03178
- Mündler, He, Wang et al., "Type-Constrained Code Generation with Language Models", PLDI 2025, ACM DL
- Blinn et al., "Statically Contextualizing Large Language Models with Typed Holes", OOPSLA 2024, ACM DL
- Sun et al., "A Benchmark for Vericoding: Formally Verified Program Synthesis", arXiv:2509.22908
- Allan, "VeraBench: a benchmark for LLM code generation in Vera", github.com/aallan/vera-bench