# AGENTS.md — Instructions for AI agents

This document is for AI agents working with the Vera codebase. There are two audiences: agents writing Vera code, and agents working on the compiler.

## For agents writing Vera code

Read `SKILL.md` for the full language reference. It covers syntax, slot references, contracts, effects, common mistakes, and working examples that all parse correctly.

### Conformance programs as reference

The conformance suite in `tests/conformance/` contains small, self-contained programs — named by spec chapter and feature (`chNN_feature.vera`) — that serve as minimal working examples (most are fully self-contained; the cross-module programs of Chapters 7–9 import companion `_lib`/module fixtures). Each positive program must pass its declared verification level (see `manifest.json` for mappings: `parse`, `check`, `verify`, or `run`); the negative fixtures (the entries with `expected_error` in `tests/conformance/manifest.json`) instead must *fail* with the E-code in their `expected_error` field, at the stage their `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses. When you need to see how a specific construct works (e.g. effect handlers, match expressions, closures), check the corresponding conformance program before reading the spec.

### Workflow

```text
write .vera file -> vera check -> fix errors -> vera verify -> fix errors -> done
```

Use **typed holes** (`?`) to build programs incrementally. A `?` in any expression position is valid — `vera check` reports a `W001` warning with the expected type and all available slot bindings:

```text
warning: [W001] Warning at file.vera, line 6, column 3:

      ?
      ^

  Typed hole: expected Int.

  ? is a placeholder for an incomplete expression. The compiler reports the expected type and available bindings so the hole can be filled in.

  Fix:

    Replace ? with an expression of type Int. Available bindings: @Int.0: Int; @Int.1: Int.

  See: Chapter 4, Section 4.17 "Typed Holes"
```

Programs with holes type-check (`ok: true`) but cannot compile (`E614`). Iterative workflow:

```text
write skeleton with ? -> vera check (get W001 hints) -> fill holes -> vera check -> vera verify
```

### Commands

```bash
vera check file.vera              # Parse and type-check
vera check --json file.vera       # Type-check with JSON output (for parsing)
vera verify file.vera             # Type-check + verify contracts via Z3, then compile
                                  #   and check each Tier 3 claim has its check (E541)
                                  #   and each check a record (W004)
vera verify --json file.vera      # Verify with JSON output (for parsing)
vera verify --timeout-ms 60000 file.vera  # Per-query Z3 budget in ms (default
                                  #   10000; env VERA_Z3_TIMEOUT_MS)
vera verify --no-reconcile file.vera  # Verify without compiling: no reconciliation
vera compile file.vera                    # Compile to .wasm binary
vera compile --wat file.vera              # Print WAT text (human-readable WASM)
vera compile --target browser file.vera   # Compile + emit browser bundle
vera run file.vera                # Compile and execute (calls main)
vera run file.vera --fn f -- 42   # Call function f with argument 42
vera serve file.vera              # Serve handle(Request -> Response) over HTTP (default :8000)
vera test file.vera               # Contract-driven testing via Z3 + WASM
vera test --json file.vera        # Test with JSON output
vera test --trials 50 file.vera   # Limit trials per function (default 100)
vera test --distrust file.vera    # Also execute proved functions; a failed proved check refutes the proof (E703)
vera fmt file.vera                # Format to canonical form (stdout)
vera fmt --write file.vera        # Format in place
vera fmt --check file.vera        # Check if already canonical
vera version                      # Print the installed version (also --version, -V)
vera lsp                          # Serve LSP over stdio (needs the [lsp] extra; see LSP_SERVER.md)
vera builtins [--json]            # List the built-in function registry (no file needed)
vera effects [--json]             # List the effect and ability registry (no file needed)
vera errors [--json]              # List the diagnostic-code registry (no file needed)
```

See [TOOLCHAIN.md](TOOLCHAIN.md) for the CLI cookbook — driving the toolchain to write, verify, test, run, and debug Vera, including the `builtins`/`effects`/`errors` introspection commands.

### The language server: proof deltas without re-running the CLI

For long editing sessions, `vera lsp` (install: `pip install -e ".[lsp]"`) keeps a warm incremental Z3 session alive, so verification feedback arrives at editor latency instead of cold-start latency. Any LSP client gets diagnostics (same error codes as `--json`), per-function verification-tier hints, hover types, slot go-to-definition, and typed-hole completion.

Four custom methods exist specifically for agents — full request/response shapes in [LSP_SERVER.md](LSP_SERVER.md):

| Method | Question it answers |
|---|---|
| `vera/speculativeEdit` | "Would this edit keep, break, or strengthen the proofs?" — in-memory verify, returns a proof delta, touches nothing |
| `vera/proposeEdit` | "Apply this edit *iff* it verifies" — the gate cannot be skipped; `force: true` overrides loudly |
| `vera/strengthenContract` | "Tighten this contract — do all call sites still satisfy it?" — refusals point at the breaking call sites |
| `vera/addEffect` | "Thread this effect through every transitive caller" — one verified multi-site rewrite, all-or-nothing |

The intended loop: draft → `speculativeEdit` → inspect the delta → `proposeEdit`. Prefer the two structured refactors over hand-editing contracts/effect rows — the server constructs the candidate and audits the blast radius for you.

### Error handling

Error messages are natural language instructions explaining what went wrong and how to fix it. They include the offending source line, a rationale, a concrete code fix, a spec reference, and a stable error code. Feed the full error back into your context to correct the code.

For machine-parseable errors, use the `--json` flag:

```json
{
  "ok": false,
  "file": "example.vera",
  "diagnostics": [
    {
      "severity": "error",
      "description": "Function is missing its contract block...",
      "location": {"file": "example.vera", "line": 12, "column": 1},
      "source_line": "private fn add(@Int, @Int -> @Int)",
      "rationale": "Vera requires all functions to have explicit contracts...",
      "fix": "Add a contract block after the signature:\n\n  private fn example(@Int -> @Int)\n    requires(true)\n    ensures(@Int.result >= 0)\n    effects(pure)\n  {\n    ...\n  }",
      "spec_ref": "Chapter 5, Section 5.2 \"Function Declaration Syntax\"",
      "error_code": "E001"
    }
  ],
  "warnings": []
}
```

### Error codes

Diagnostics carry stable codes, which `vera errors` lists; a few diagnostics carry none. Common codes:

| Code | Meaning |
|------|---------|
| W001 | Typed hole (`?`) — expected type and available bindings reported |
| E001 | Missing contract block (requires/ensures/effects) |
| E020 | Unterminated block comment — `{-` with no matching `-}` (they nest, so each needs its own closer) |
| E121 | Function body type doesn't match return type |
| E130 | Unresolved slot reference (`@T.n` has no matching binding) |
| E140 | Arithmetic requires numeric operands |
| E170 | Let binding type mismatch |
| E200 | Unresolved function call |
| E300 | If condition is not Bool |
| E311 | Non-exhaustive match |
| E614 | Program contains typed holes — compile rejected until holes are filled |

Full code ranges: W0xx (warnings), E0xx (parse), E1xx (type/expressions), E2xx (calls), E3xx (control flow), E5xx (verification), E6xx (codegen), E7xx (testing). See `vera/errors.py` `ERROR_CODES` for the complete registry.

The `verify --json` output includes a verification summary:

```json
{
  "ok": true,
  "file": "example.vera",
  "diagnostics": [],
  "warnings": [],
  "verification": {
    "tier1_verified": 2,
    "tier3_runtime": 0,
    "assumptions": 0,
    "total": 2
  }
}
```

Alongside it, an `obligations` array carries one entry per reified proof obligation (`kind`, `status`, `description`, `location`). The summary is derived from that array by `status` — `verified` counts as `tier1_verified`, `tier3`/`timeout` as `tier3_runtime`, and `total` is their sum. Reproduce the counts by *filtering on `status`*, not by taking the array's length: a `violated` or `tier3_unguarded` obligation discharged to no tier, so it is counted nowhere and is surfaced as an error or warning diagnostic instead. On a program with one refuted contract, `total: 2` beside a three-entry array is the expected partition.

`assumptions` sits beside those counts and is NOT part of that identity: it counts the `assume` statements this run took on trust (one W003 warning each, spec §6.2.6), which are not obligations and discharge to no tier. It is derived from the assembled diagnostics, so a consumer reproduces it by counting W003 rather than by reading any obligation's status. A non-zero value is the honest measure of how much of a "verified" result rests on something nobody proved.


### Essential rules

1. Every function needs `requires()`, `ensures()`, and `effects()` between the signature and body
2. Use `@Type.index` to reference bindings (`@Int.0` = most recent Int, `@Int.1` = one before)
3. Declare all effects: `effects(pure)` for pure functions, `effects(<IO>)` for IO, `effects(<Http>)` for network, `effects(<Inference>)` for LLM calls
4. `Http.get(@String.0)` and `Http.post(@String.0, @String.1)` return `Result<String, String>`; match the result
5. `Inference.complete(@String.0)` returns `Result<String, String>`; requires `VERA_ANTHROPIC_API_KEY`, `VERA_OPENAI_API_KEY`, `VERA_MOONSHOT_API_KEY` (Kimi), `VERA_MISTRAL_API_KEY`, `VERA_XAI_API_KEY` (Grok), or `VERA_DEEPSEEK_API_KEY` to run; provider auto-detected from whichever key is set to a non-empty value.  See [`ENVIRONMENT.md`](ENVIRONMENT.md) for the full env-var reference, including `VERA_INFERENCE_PROVIDER` / `VERA_INFERENCE_MODEL` overrides
6. Recursive functions need a `decreases()` clause
7. Match expressions must be exhaustive
8. `DB.query` / `DB.execute` (effect `<DB>`) take a **literal** SQL string — a query assembled from a runtime value is a compile-time error (`E207`). Every runtime value goes through a `?` placeholder and the `Array<Option<String>>` params array (`DB.query("SELECT ... WHERE id = ?", [Some(@String.0)])`); a placeholder/params count mismatch with a literal params array is `E208`. The connection comes from `VERA_DB_URL` (default: in-memory SQLite) — see [`ENVIRONMENT.md`](ENVIRONMENT.md)

## For agents working on the compiler

Read `vera/README.md` for architecture docs, module map, and design patterns.

### Pipeline

```
source -> parse (parser.py) -> transform (transform.py) -> resolve (resolver.py) -> typecheck (checker/) -> verify (verifier.py) -> compile (codegen/ + wasm/) -> execute (wasmtime or browser/runtime.mjs)
```

Each stage is a module with a single public API function (`parse_file`, `transform`, `resolve_imports`, `typecheck`, `verify`, `compile`, `execute`, `test`) and is independently testable.

### Key modules

| Module | Purpose |
|--------|---------|
| `vera/grammar.lark` | Lark LALR(1) grammar |
| `vera/parser.py` | Parser: source text to Lark parse tree |
| `vera/transform.py` | Lark tree to typed AST |
| `vera/ast.py` | AST node definitions |
| `vera/types.py` | Internal type representation |
| `vera/environment.py` | Type environment and slot resolution |
| `vera/checker/` | Type checker (mixin package) |
| `vera/smt.py` | Z3 SMT translation layer |
| `vera/verifier.py` | Contract verifier |
| `vera/registration.py` | Shared function registration for checker and verifier |
| `vera/errors.py` | LLM-oriented diagnostics |
| `vera/wasm/` | WASM translation layer (mixin package) |
| `vera/codegen/` | Code generation orchestrator (mixin package) |
| `vera/tester.py` | Contract-driven testing engine |
| `vera/cli.py` | Command-line interface |
| `vera/markdown.py` | Markdown parser (host-side implementation) |
| `vera/browser/` | Browser runtime: JS host bindings, Node.js harness, bundle emission |

### Testing

```bash
pytest tests/ -v                       # Run all tests (see TESTING.md)
pytest tests/test_conformance.py -v    # Conformance suite only
mypy vera/                             # Type-check the compiler
python scripts/check_conformance.py    # Every conformance program holds (positives pass; negatives fail with their E-code)
python scripts/check_examples.py       # Every example must pass
python scripts/check_corpus_canonical.py # Every corpus program in canonical form
```

Test helpers follow a pattern: `_check_ok(source)` / `_check_err(source, match)` / `_verify_ok(source)` / `_verify_err(source, match)`. See existing tests for examples.

When implementing a new language feature, write the conformance program *first* — add a `.vera` file and manifest entry in `tests/conformance/`, then implement the feature until the conformance test passes.  A `run`-level entry pins its run: `expected_stdout`, exactly what the program must print, and `expected_exit`, or a `nondeterministic_stdout` reason in place of `expected_stdout` (TESTING.md § Manifest).

When one mechanism bounds a bug's class, the fix closes the **class** the report belongs to, not the reported instance, in the same pull request and bounded to that mechanism: name the class boundary in the PR body and ship a class instrument — an exhaustive matrix over the space the class spans, or a generator — rather than hand-picked cases.  A class whose boundary is architectural, two phases re-deriving the same fact, is not fixed per site: its issue carries the milestone of the release that removes the mechanism, and closes there.  A class instrument is a burndown tool: its file carries the `matrix` marker, naming the modules that decide its class; the nightly lane and any pull request that changes the file or one of those modules run it in full, and every other pull request runs a stratified sample of its cells, pinned for a week.  Review is capped at three rounds; a fourth needs a written answer to "which mechanism produces these members, and does this PR remove it?".  One issue per class, with its instances as a checklist.  See `CONTRIBUTING.md` § Bugs: the class, not the instance, and `TESTING.md` § Class Instruments.

### Invariants

- Every conformance program in `tests/conformance/` must hold at its declared level — positive entries pass, and the negative fixtures (the entries with `expected_error` in `tests/conformance/manifest.json`) must *fail* with their `expected_error` E-code, at the stage `expected_error_stage` names — `check` by default, or `compile` for a diagnostic the checker accepts and codegen refuses, which also asserts the program type-checks cleanly first
- Every example in `examples/` must pass `vera check` and `vera verify`
- `mypy vera/` must be clean
- `pytest tests/ -v` must pass
- The version is written in `pyproject.toml` alone: `vera.__version__` reads the installed metadata, and `uv lock --check` holds `uv.lock`'s own entry to it; a release also needs a matching `## [X.Y.Z]` section in CHANGELOG.md, which `scripts/release.py` requires

### Releases and install docs

**Releases are automated after merge.** A version bump on `main` (`[project].version` in `pyproject.toml`, with a matching non-empty `CHANGELOG.md` section) triggers `.github/workflows/release.yml`: it builds, waits for the maintainer to approve the protected `pypi` environment, publishes to PyPI via Trusted Publishing, then creates the tag and GitHub Release at the merge SHA. Do NOT create tags, run `twine`, or `gh release create` — the maintainer and the workflow own that. See `CONTRIBUTING.md` §Releases and `RELEASING.md`.

**Install docs are circumstance-dependent — match `README.md`, `SKILL.md`, and `PYPI_README.md`; don't invent "the install route".** The GitHub source checkout (`pip install -e .`, plus `[lsp]` or `[dev]`) is the full environment — the toolchain alongside `examples/`, `tests/conformance/`, and `spec/` — and is the recommended route for agents; `pip install veralang` installs the toolchain only; the `[lsp]` extra adds the language server; never write `pip install vera` (an unrelated PyPI project). Only document a channel as an available install route once the artifact is live there **and** the install flow works end to end — check the registry, don't rely on what you remember. The VS Code extension meets that bar: [`veralang.vera-language`](https://marketplace.visualstudio.com/items?itemName=veralang.vera-language) installs from the Marketplace, in the Extensions view or via `code --install-extension veralang.vera-language`. The same gate applies to any future distribution channel.

### Contributing

See `CONTRIBUTING.md` for guidelines. Pre-commit hooks run the fast gates on every commit — ruff, mypy, trailing whitespace checks, the doc gates, and the test files the commit stages; CI runs the full test suite, the conformance suite and every example on every pull request.