Vera.

The thesis.

Vera takes the verification camp’s diagnosis literally. If LLMs make semantic errors faster than humans can catch them by reading code, the compiler has to do the catching. Every function declares preconditions, postconditions and an effect row, and the compiler sorts each resulting obligation into a three-tier scheme: Z3’s decidable fragment, Z3 guided by hints, or a compiled runtime check. What can be proved statically is proved before anything runs; what cannot is checked as the program executes.

The model doesn't need to be right. It needs to be checkable.

The distinctive move is replacing variable names with typed slot references. A function safe_divide(@Int, @Int -> @Int) has no parameter names — its arguments are referred to as @Int.0 (most recent) and @Int.1 (next most recent) using De Bruijn indexing. The grammar has nowhere to put a parameter name at all, which is what separates Vera from the two catalogue entries that reached De Bruijn indices later: Tacit, in April, keeps display names in a sidecar, and LLMLang, in May, lets its parser accept them before resolving to indices.

The project grounds the choice in two papers. Wang et al. (arXiv:2307.12488) replaced identifiers in code-analysis tasks and found that good names help a model, but that shuffled names — count swapped with result — hurt it more than gibberish does. Le et al. (arXiv:2510.03178) describe identifier leakage, where a model appears to understand code while pattern-matching on familiar tokens. Vera’s reading, set out in its FAQ, treats names as a crutch worth removing rather than an aid worth improving.

What it looks like.

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

Distinctive moves.

• Mandatory contracts. Every function carries requires/ensures/effects clauses. There’s no opt-out; the grammar rejects functions without them. Nine catalogue entries now enforce something per function, so the live differentiator sits in what discharges the obligations rather than in their being compulsory.
• De Bruijn slot references. No variable names at the parameter level. @T.n denotes the n-th-most-recent binding of type T. vera check --explain-slots prints the resolution table when the indices stop being obvious.
• Typed effects, including inference. LLM calls are an <Inference> effect dispatching to Anthropic, OpenAI, Moonshot or Mistral. A function that doesn’t declare it can’t make model calls, and the effect system tracks model usage up the call graph. Ten effects ship in total, alongside four abilities.
• Three-tier verification, two tiers shipped. Tier 1 sends an obligation to Z3’s decidable fragment on a ten-second budget; Tier 3 compiles it into a runtime check. Tier 2 — Z3 guided by assert and lemma hints — is specified in chapter 6 and not implemented, so contracts needing hints fall through to Tier 3. Obligations also degrade to Tier 3 on a solver timeout, an opaque effect result or a dynamic array length; vera verify --json reports the two live buckets, tier1_verified and tier3_runtime.
• SQL injection as a compile error. The <DB> effect requires literal provenance for query text: a query assembled from a runtime value is E207 at check time. The guarantee needs no solver, which is why the project notes it holds inside handled code where solver-based claims cannot reach.
• LLM-oriented diagnostics. Every error code is stable (E001–E702); every diagnostic carries a rationale, a fix hint and a spec reference, gated in CI since v0.0.188. The CLI emits JSON for tooling.

Maturity.

At v0.1.9 (5 August 2026) after 205 tagged releases and roughly 2,400 commits. The project reports 9,382 tests at 95% coverage, 196 conformance programs — which it describes as validating every language feature, across nine of the fourteen spec chapters — 42 examples, 164 built-in functions and a 14-chapter draft specification. The test count reproduces from a pytest --collect-only run; the enforced CI coverage floor is 80%, with 95% the project’s own measurement. v0.1.0 shipped on 4 July with an empty bug tracker after 37 bug-labelled issues closed on a single branch. The reference compiler is Python; programs compile to WebAssembly and execute under wasmtime, in the browser via a self-contained bundle with mandatory parity tests, or on stock WASI Preview 2 hosts, where --world server packages a contract-verified handle(Request -> Response) as a wasi:http component that unmodified wasmtime serve will run.

VeraBench, which the project authors, runs and grades, published a fresh sweep on 28 July 2026: nine model configurations across three providers, all 60 problems graded for the first time. It reports Vera averaging 98.7% solved against Python’s 96.7% and TypeScript’s 99.7%, with two further zero-training-data languages, Aver and AILANG, as comparison baselines. The project publishes the caveats alongside the numbers: a single run per model and no pass@k, one problem worth 1.7 percentage points so that most gaps are one or two problems wide, an uncontrolled generation trend, and a benchmark it calls saturated, since TypeScript scores 100% for eight of the nine configurations and Vera for six. The framing to hold onto is the project’s own — Vera earns close to TypeScript’s score “from a single skill file in context”, so the comparison sets a specification supplied at evaluation time against languages the models already know. Result files are not checked in, so the figures are not reproducible from the repository.

Current work runs dual-threaded: a verification-completeness sprint closing cases where an obligation goes unemitted or a guard unplanted, and a single-source sprint putting drift-prone facts behind one generator or gate. The most recent merge consolidated slot naming into a single renderer after six subsystems were found disagreeing about type aliases — a naming bug class inside a language that removed names. Open questions include Tier 2, postcondition and refinement facts lost through ADT fields, and production controls for the <Http> and <Inference> effects. The language server, a VS Code Marketplace extension, Vim and Neovim packages and a PyPI distribution all ship; a Vera package registry does not.

Agent tooling.

Three documents target agent authors directly: SKILL.md (a ~119 KB language reference for agents writing Vera), AGENTS.md (setup for any agent system) and CLAUDE.md (orientation for Claude Code). veralang.dev carries the machine-readable companions — llms.txt, llms-full.txt (essentially SKILL.md, ~193 KB), a markdown companion to the landing page, and an ai-plugin.json manifest; AGENTS.md is linked from the index rather than inlined, and CLAUDE.md stays in the repository. Diagnostics emit JSON carrying description, rationale, fix, spec_ref and a stable error_code, alongside a per-obligation tier tally. vera builtins, vera effects and vera errors expose the compiler’s own registries as JSON, so an agent can enumerate the language rather than infer it. The language server adds four methods addressed at agents rather than editors — vera/speculativeEdit, vera/proposeEdit, vera/strengthenContract and vera/addEffect — each answering whether an edit keeps, breaks or strengthens the program’s proofs.