vera: Instructions file for Claude Code

CLAUDE.md — Project orientation for Claude Code

Vera is a programming language designed for LLMs to write. It has mandatory contracts, algebraic effects, typed slot references (@T.n), and compiles to WebAssembly. The reference compiler is written in Python.

Virtual environment

Always use the project venv. All commands below assume it is active:

source .venv/bin/activate

If the venv does not exist, create it first:

python -m venv .venv && source .venv/bin/activate && pip install -e ".[dev]"

If you prefer uv, use uv sync --extra dev (not plain uv sync). The [dev] extras group holds pytest, mypy, ruff, pre-commit, and pip-licenses; uv sync without --extra dev will quietly uninstall those and make pytest fall through to a non-venv copy that can't import vera.

Key commands

vera check file.vera              # Parse and type-check
vera check --json file.vera       # Type-check with JSON diagnostics
vera check --quiet file.vera      # Type-check, suppress success output
vera check --explain-slots file.vera  # Show slot resolution table (which @T.n maps to which param)
vera verify file.vera             # Type-check + verify contracts via Z3, then compile in
                                  #   process and check every Tier 3 claim against the
                                  #   checks the module holds (E541 claim with no check,
                                  #   W004 check with no record)
vera verify --json file.vera      # Verify with JSON diagnostics
vera verify --quiet file.vera     # Verify, suppress success output
vera verify --timeout-ms 60000 file.vera  # Per-query Z3 budget in ms (default 10000;
                                  #   env VERA_Z3_TIMEOUT_MS; raise it to tell a
                                  #   needs-more-time Tier 3 from a never one, #1350)
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 compile --target wasi-p2 file.vera   # Emit a WASI Preview 2 component (IO+Random; #237)
vera run file.vera                # Compile and execute (calls main)
vera run file.vera --fn f -- 42   # Call function f with argument 42
vera run --target wasi-p2 file.vera  # Execute under the built-in WASI 0.2 host (spec/13-wasi.md)
vera compile --target wasi-p2 --world server file.vera  # wasi:http server component for `wasmtime serve` (spec §13.7)
vera serve file.vera              # Serve handle(Request -> Response) over HTTP (#305)
vera serve --port 8080 file.vera  # Serve on a specific port (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 parse file.vera              # Print the parse tree
vera ast file.vera                # Print the typed AST
vera ast --json file.vera         # Print the AST as JSON
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 lsp                          # Serve LSP over stdio (needs the [lsp] extra; see LSP_SERVER.md)
vera version                      # Print the installed version (also --version, -V)
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)

pytest tests/ -v                  # Run the test suite (see TESTING.md); each class-instrument matrix runs its sample
pytest tests/ -v --matrix=full    # The same, with every cell of every class-instrument matrix
VERA_JS_COVERAGE=1 pytest tests/test_browser.py -v  # Browser tests with JS coverage
VERA_EAGER_GC=1 vera run file.vera  # Force GC on every alloc (see ENVIRONMENT.md, debug knob for #593-class GC-rooting bugs)
VERA_DEBUG_HOST_ERRORS=1 vera run file.vera  # Re-raise a host callback's own exception (see ENVIRONMENT.md, debug knob for host-binding bugs)
mypy vera/                        # Type-check the compiler itself

python scripts/check_conformance.py    # Verify every conformance program (positives pass their level; negatives fail with their expected_error E-code)
python scripts/check_examples.py      # Verify every example parses + checks + verifies
python scripts/check_examples_run.py  # Run every runnable example trap-free under the native runtime; the rest carry a documented skip property, and an example that is neither is an error
python scripts/check_reconciliation.py # Reconcile every corpus program's runtime-check claims (`tier3`) with the checks its compiled module holds (the audit's T2a); fails on a mismatch outside its KNOWN allowlist, keyed by open issue, or on a KNOWN entry the join no longer reports
python scripts/check_corpus_canonical.py # Verify every corpus program is in canonical form (vera fmt)
python scripts/check_examples_readme.py # Verify vera run commands in examples/README.md
python scripts/check_doc_examples.py  # Verify every Vera block in the agent-facing docs (SKILL.md, README, FAQ, EXAMPLES.md, DE_BRUIJN.md, PYPI_README, spec/, docs/index.html + index.md) parses, passes vera check (no warning outside a named benign set) + vera verify, and prints what each vera:run marker says it prints — or carries a vera:skip marker naming the stage and codes it fails with; a block that exports a function names a vera:run invocation or a vera:no-run property; every `vera run examples/...` a doc names is run unless check_examples_run.py already runs it or skips that example by property; also fails when a tracked doc with Vera blocks is in neither DOC_GATES nor NOT_GATED (#1481)
python scripts/check_doc_examples.py SKILL.md  # The same gate, for the named documents only
python scripts/check_diagnostic_examples.py # Verify every vera:diagnostic-annotated ```text fence matches the live diagnostic it shows (#1291)
python scripts/check_doc_builtin_shadowing.py # Verify no doc example redefines a built-in (E151; #819)
python scripts/check_diagnostic_fields.py # Verify every diagnostic carries rationale + spec_ref (+ fix for errors; warnings exempt) or a # diag-fields-exempt reason — waives missing/unresolvable fields only, never a factually wrong spec_ref/error_code (#682)
python scripts/check_explicit_encoding.py # Verify every text-mode open()/read_text()/write_text() passes explicit encoding='utf-8' (#645)
python scripts/build_site.py          # Regenerate AI-readable site assets (llms.txt, etc.)
python scripts/check_site_assets.py   # Verify site assets are up-to-date + docs/index.html ↔ docs/index.md state coherent facts (#1154)
python scripts/render_status.py      # The release PR: write TESTING.md's generated status (where the counts live) from the tree
python scripts/check_doc_counts.py --release # The release PR: TESTING.md's generated status and every render_lists block are current (CI runs this mode on any change that raises [project].version, via --release-if-version-raised)
python scripts/render_lists.py --write  # Write the lists that have one source between their render_lists markers: the effect names from the registry into the editor grammars and extension READMEs, the limitation tables from limitations.json
python scripts/render_lists.py --check  # Name each render_lists block that is not what --write writes (the release check above runs it)
python scripts/check_doc_counts.py --check-bug-issues # The release PR: KNOWN_ISSUES' Bugs table against the open `bug` issues (GitHub API)
python scripts/check_corpus_differential.py --base-ref origin/main  # Compile the corpus at two revisions; report programs whose WAT moved (burndown instrument, not a hook)
python scripts/check_licenses.py      # Verify all package licenses are MIT-compatible
python scripts/check_wheel_availability.py # Verify every runtime dep has wheels for all supported platforms (README §Supported platforms)
python scripts/check_limitations_sync.py              # Verify limitations.json loads and the KNOWN_ISSUES.md and SKILL.md Bugs headings survive (offline)
python scripts/check_limitations_sync.py --check-states # Also verify every issue they cite is still open via GitHub API (limitations-sync.yml runs it weekly)