Summary

Add a new CLI command vera context that exports a compact, token-budgeted summary of a Vera project's public API surface for consumption by LLM agents working on or with a codebase written in Vera.

Directly inspired by Aver's aver context command. Credit Szymon Teżewski's aver context design in the implementation, the commit message, and the CLI help text.

Why this fits Vera especially well

Every Vera function already carries mandatory, machine-readable contracts. The output for each public function looks like:

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)

Four lines communicate: parameter types, preconditions, postconditions, and effects. An LLM reading this knows everything it needs to call the function correctly — no need to read the body. In a named-variable language you'd additionally need to convey parameter names and their semantic meaning. In Vera the types and contracts carry all of that.

The De Bruijn slot notation makes signatures compact. The mandatory contracts make the summaries self-documenting. The effect system tells you at a glance whether a function does IO, HTTP, inference, or is pure.

Aver's design (the reference)

From the Aver README context-export section:

Aver walks the dependency graph and emits a compact context summary: module intent, public signatures, effect declarations, verify samples, and decisions. The goal is not to dump the whole source tree; it is to export the contract-level view that another human or LLM needs first.

Key design details adopted here:

• Default: --depth auto --budget 10kb — tries depth 0, 1, 2, … and keeps the deepest result that fits the byte budget.
• Budget as navigation primitive: the byte budget is a first-class parameter so an LLM can start with a small architecture map and zoom into specific modules rather than reading the whole tree.
• Graceful truncation: long verify examples are skipped rather than bloating the artefact. Selection metadata is embedded in the output so callers can see whether the export was truncated.
• Override controls: --depth N and --depth unlimited bypass auto; --budget 24kb (etc.) raises the ceiling.
• Output formats: text (default) and --json for machine consumption.

Read the Aver README in full before designing the Vera implementation: https://github.com/jasisz/aver

Proposed CLI

vera context [entry_file] [options]

Options:

• --budget SIZE — maximum output size (default 10kb). Accepts 10kb, 24kb, 64kb, etc.
• --depth N — fixed dependency depth. auto (default) tries increasing depths within budget. unlimited exports everything.
• --json — emit structured JSON instead of text.
• --output FILE — write to file instead of stdout.

Output per module

1. Module path (file/module identifier).
2. Public function signatures with full contracts — signature, requires, ensures, effects, and decreases (if recursive). No bodies.
3. Public ADT definitions — type constructors and fields.
4. Effect declarations — any custom effects defined in the module.
5. Import list — what this module depends on.

Budget algorithm

Mirrors Aver:

1. Start at depth 0 (entry module only).
2. Render the context at this depth.
3. If it fits within the budget, try depth + 1.
4. Keep the deepest result that fits.
5. Embed metadata indicating whether the export was truncated and at what depth.

Example output (text)

# vera context — budget: 10kb, depth: auto (resolved: 1)

## Module: src/main.vera

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)

public fn classify_sentiment(@String -> @Result<String, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Inference>)

public fn research_topic(@String -> @Result<String, String>)
  requires(string_length(@String.0) > 0)
  ensures(true)
  effects(<Http, Inference>)

type Document = { title: @String, body: @String, tags: @Array<String> }

## Module: src/utils.vera (depth 1, imported by main.vera)

public fn format_output(@String, @Int -> @String)
  requires(true)
  ensures(string_length(@String.result) > 0)
  effects(pure)

--- truncated at depth 1 (budget: 10kb, used: 3.2kb) ---

Example output (JSON)

{
  "budget": "10kb",
  "depth_requested": "auto",
  "depth_resolved": 1,
  "truncated": false,
  "used_bytes": 3247,
  "modules": [
    {
      "path": "src/main.vera",
      "depth": 0,
      "functions": [
        {
          "name": "safe_divide",
          "visibility": "public",
          "signature": "@Int, @Int -> @Int",
          "requires": "@Int.1 != 0",
          "ensures": "@Int.result == @Int.0 / @Int.1",
          "effects": "pure"
        }
      ],
      "types": [],
      "imports": ["src/utils.vera"]
    }
  ]
}

Relationship to existing agent tooling

This sits alongside but is distinct from:

• SKILL.md — teaches an agent the Vera language itself (syntax, slot references, contracts, common mistakes). Language documentation.
• AGENTS.md / CLAUDE.md — teach an agent how to work on the Vera compiler or write Vera code. Project documentation.
• vera context — teaches an agent a specific project written in Vera. Project-specific API surface export.

The three are complementary. An agent working on a Vera project uses SKILL.md to understand the language, CLAUDE.md to understand the development workflow, and vera context to understand the specific codebase it's working on.

Roadmap placement

Milestone 3: Tooling for real-world adoption, Phase 3a (Agent integration) — alongside the LSP server (#222) and Plumbing integration (#329). Not a current-sprint item — the ongoing bug campaign and stdlib breadth work should complete first — but a natural next step once projects start having multiple files.

Estimated effort: 1–2 days, given that the module system and function registry already exist in the compiler internals.

Credit

Directly inspired by Szymon Teżewski's aver context command in the Aver programming language (https://github.com/jasisz/aver). The token-budget-as-navigation-primitive insight is his. We are adapting the concept for Vera's contract-first architecture, where the mandatory contracts make the exported summaries richer per byte than would be possible in a language without them.