Assura for AI agents

Assura is built so agents can propose implementations and the compiler can accept or reject them with structured evidence.

Install

cargo install assura --locked
assura --help

Docs site: https://assura-lang.github.io/assura/

Core loop

1. Human (or agent) writes or edits a .assura contract.
2. Agent produces an implementation path (synthesized IR, co-located .ir, or Rust under check-rust).
3. Agent runs assura check / assura check-rust / assura build.
4. Agent reads machine-readable results and iterates on counterexamples, not on vibes.

assura check path/to/file.assura --json
assura check-rust src/ --json

Full field table and branch policy: Agent verification loop. Inline Rust surface: CHECK-RUST-SURFACE. Demos: demos/check-rust/ (prove + intentional fail).

Acceptance policy (LLM IR / auto-implement)

Do not require every clause status == "verified". Many clauses return Unknown because a feature is not yet encoded in SMT. For agent IR:

• Reject if any Counterexample appears.
• Accept when there is no counterexample (Unknown is allowed for unmodeled features). Generated Rust may still carry runtime assertions from requires/ensures codegen.

See AGENTS.md pipeline notes for verify_ir and multi-contract source pitfalls (first contract only unless single-contract source is synthesized).

Vacuous success

JSON success can still be vacuous (no contracts, or no SMT proof obligations). Inspect file_info.vacuous / vacuous_reason (and human summaries that say “no SMT proof obligations”). Do not report that as full coverage.

MCP

The assura-mcp crate exposes tools for agent hosts (rmcp). There is no standalone assura-mcp binary. Start the server from the CLI:

assura mcp

A bare terminal looks idle; MCP hosts must spawn this process. Example host config:

{
  "mcpServers": {
    "assura": {
      "command": "assura",
      "args": ["mcp"]
    }
  }
}

Tools: assura_check, assura_infer, assura_explain, assura_type_map, assura_ir_prompt, assura_ir_verify. List them from your MCP client after connecting. Prefer assura check --json when MCP is unavailable.

The official MCP Registry entry is published from server.json on a release, after that version of the assura crate is on crates.io and its README contains mcp-name: io.github.assura-lang/assura. The publish job is Publish MCP Registry. A copy of server.json in git does not by itself create the listing.

Glama indexes public GitHub repos. glama.json names the maintainers (SebTardif). That file does not create the directory entry. A signed-in maintainer submits https://github.com/assura-lang/assura once with Add Server. There is no Glama token and no release job. Review reads the root README. On 2026-11-08 Glama rejected the listing because that README only mentioned an MCP server as a documentation-link label. The MCP server section has to name the crate, the rmcp SDK, assura mcp on stdio, and the tools. Resubmit only after that section is on the default branch. Do not say the server is listed until https://glama.ai/api/mcp/v1/servers?query=assura returns it. The short description must match server.json: a check returns Verified, Counterexample, or Unknown.

JSON envelopes (assura_check, assura_infer)

Both tools return a JSON object, not raw diagnostic text or raw contract source. Shared fields:

assura_infer is not a raw contract string. Write result.text to a .assura file, never the whole envelope. When infer is vacuous, success is true, vacuous is true, and text is empty or a “nothing found” placeholder. Branch on vacuous (and vacuous_reason), not on success.

success: false means a real error (unknown --function on the CLI, parse/IO/LLM failure, or a jail reject below).

File jail

file / ir_file arguments must be relative to the MCP process cwd. Allowed extensions: .assura, .rs, .ir. The same extension check applies after canonicalize (a leak.rs symlink to .env is rejected). Absolute paths outside cwd, ../ escapes, missing files, and other extensions are rejected.

Rejected paths and other resolve failures return JSON (same shape as other JSON-tool errors). Branch on error_kind, not on the message string:

{"success": false, "error": "path not allowed", "error_kind": "PATH_NOT_ALLOWED", "message": "file must be inside the server working directory and use a .assura, .rs, or .ir name"}

The error string does not include the requested filesystem path. Inline source / ir text is not jailed. File reads take at most 16 MiB of actual bytes (not a metadata-only check).

Suggested agent checklist

1. Prefer showcase demos over *-audit.assura (many audits are EXPECT FAIL).
2. On failure, paste the clause description and model into the next edit.
3. Use --layer 0 for fast structural iteration when SMT is noisy.
4. Read What we prove before claiming “proved secure”.

Related

• Agent verification loop
• Getting started
• Compared to other tools
• check-rust supported surface
• Case studies
• Preferred URLs