Vera is a novel programming language engineered specifically for Large Language Models (LLMs) to author code. It addresses LLMs' inherent difficulties with maintaining coherence, reasoning about state, and managing complexity at scale by enforcing strict verifiability. The primary benefit is enabling LLMs to generate more reliable, maintainable, and correct code by shifting the burden from model memorization to compiler-checkable specifications.

How It Works

Vera replaces traditional variable names with explicit, typed De Bruijn indices (e.g., @Int.0 for the most recent Int, @Int.1 for the one before) to eliminate naming ambiguity and errors. Every function requires mandatory requires (precondition), ensures (postcondition), and effects clauses. These contracts are statically verified by the compiler using the Z3 SMT solver for decidable cases (Tier 1) or fall back to runtime checks (Tier 3). Explicitly declared algebraic effects (like Http, Inference, IO) ensure that side effects are transparent and controlled, preventing unexpected behavior. This design prioritizes mechanical checkability, allowing models to focus on generating plausible logic that the compiler can rigorously validate.

Quick Start & Requirements

• Installation: Clone the repository, create and activate a Python virtual environment, then install with pip install -e ".[dev]".
• Prerequisites: Python 3.11+, Git. Node.js 22+ is optional but recommended for browser runtime and parity tests.
• Workflow: Key commands include vera check (parse and type-check), vera verify (contract verification), vera run (compile and execute), and vera compile --target browser (create self-contained browser bundles).
• Documentation: Examples are available in EXAMPLES.md, and design rationale in FAQ.md.

Highlighted Details

• Contract Verification: Leverages Z3 for static analysis of function contracts, ensuring preconditions and postconditions are met. Tier 3 contracts provide runtime fallbacks.
• LLM-Oriented Diagnostics: Compiler errors are structured as actionable instructions for LLMs, including error codes, explanations, suggested fixes with code examples, and references to the specification.
• Browser Runtime: Compiles to WebAssembly, producing self-contained HTML/JS bundles for browser execution without external build tools.
• Agent Integration: Includes comprehensive documentation (SKILL.md, AGENTS.md, CLAUDE.md) tailored for LLM agents, facilitating code generation and compiler interaction.
• Performance Benchmarks: VeraBench results indicate LLMs achieve high correctness rates (e.g., Kimi K2.5 at 100%) on Vera programs, often surpassing Python and TypeScript implementations.

Maintenance & Community

The project is under active development (v0.0.127) with a substantial commit history (810+), numerous releases (127), extensive testing (3,638 tests, 96% coverage), and a detailed specification. A roadmap (ROADMAP.md) outlines future development. No explicit community channels (e.g., Discord, Slack) are listed.

Licensing & Compatibility

Vera is licensed under the permissive MIT License. Its direct dependencies use MIT or Apache-2.0 licenses. A single transitive dependency (chardet) uses LGPL v2+, which is compatible with MIT redistribution. This licensing permits commercial use and integration into closed-source projects.

Limitations & Caveats

The project is in active development at version v0.0.127. Known bugs and open issues are tracked in KNOWN_ISSUES.md. Tier 3 contract verification relies on runtime checks rather than static guarantees.