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

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:

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:

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

Commands

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
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 --reconcile file.vera # Also compile, and check each Tier 3 claim has
                                  #   its check (E541) and each check a record (W004)
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 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:

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:

{
  "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:

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:

{
  "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 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

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

Testing

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 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.