Assura
OfficialServer Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
Assura contract-first AI-native language tools. Use assura_check to verify contracts, assura_infer to generate contracts from Rust code, assura_ir_prompt to generate Implementation IR prompts, assura_ir_verify to verify IR implementations against contracts (AI verification loop), assura_explain to look up error codes, and assura_type_map to convert Rust types.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| assura_checkA | Parse, type-check, and verify an Assura contract. Returns structured diagnostics and verification results. Provide either |
| assura_explainA | Explain an Assura error code. Returns the error name, description, example, and suggested fix. |
| assura_inferA | Infer skeleton Assura contracts from Rust source code. Provide either |
| assura_ir_promptB | Render an AI prompt to generate Implementation IR (.ir sidecar) for an Assura contract. Provide |
| assura_ir_verifyA | Verify an Implementation IR against an Assura contract using SMT solvers (Z3/CVC5). Returns per-clause verification results with counterexamples and progress tracking. The core tool for the AI verification loop: generate IR, submit for verification, and read feedback. Stop when there is no Counterexample. Unknown is acceptable because some features are not encoded in SMT; do not keep rewriting the IR because a clause is Unknown. Provide contract via |
| assura_type_mapA | Map a Rust type to the equivalent Assura type (e.g. Vec -> List). |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored across 6 tools
Each tool targets a distinct stage of the verification workflow: check (contract verification), ir_verify (IR verification), ir_prompt (IR generation prompt), infer (contract inference), type_map (type conversion), and explain (error lookup). The closest pair is assura_check and assura_ir_verify, but the descriptions clearly distinguish whole-contract verification from Implementation IR clause checking.
All tools share the assura_ prefix and snake_case, which gives a predictable namespace. The suffixes mix verbs (check, infer, explain) with noun-ish compounds (ir_verify, ir_prompt, type_map), a minor deviation but still readable and grouped by the ir_ family.
Six tools is well-scoped for a contract verification server, with each tool corresponding to a clear step (infer, type map, prompt, verify, check, explain). No tool feels redundant or trivial.
The surface covers the full loop: infer a contract from Rust, map types, render an IR prompt, verify IR, check contracts, and explain errors. Minor gaps exist, such as no tool to apply or auto-fix diagnostics or to list/decompose multi-contract files beyond the decl parameter.