GoKawiilVera
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 }
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.
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.
... continue reading