Assura
Check Assura contracts with Z3. Returns Verified, Counterexample, or Unknown.
- GitHub stars
- 9
- tools
- 6
- transport
- STDIO
- last updated
- Nov 9, 2026
Tools
6 toolsPublic tool metadata for what this MCP can expose to an agent.
assura_checkParse, type-check, and verify a contract. Pass `source` or `file`.
Parse, type-check, and verify a contract. Pass `source` or `file`.
No parameter schema in public metadata yet.
assura_inferInfer skeleton contracts from Rust source.
Infer skeleton contracts from Rust source.
No parameter schema in public metadata yet.
assura_explainExplain an Assura error code.
Explain an Assura error code.
No parameter schema in public metadata yet.
assura_type_mapMap a Rust type such as `Vec<i64>` to an Assura type.
Map a Rust type such as `Vec<i64>` to an Assura type.
No parameter schema in public metadata yet.
assura_ir_promptRender a prompt that asks for Implementation IR.
Render a prompt that asks for Implementation IR.
No parameter schema in public metadata yet.
assura_ir_verifyCheck that IR against the contract with Z3 or CVC5.
Check that IR against the contract with Z3 or CVC5.
No parameter schema in public metadata yet.
Sponsors
Agent CaffeineSponsoredClose your lid, come back to finished work
SnugSponsoredThe clipboard manager for the AI eraPromote your product hereReach 125k+ visitors monthly
WaxSponsoredBlock anything with supervision, without erasing your iPhonePromote your product hereReach 125k+ visitors monthly
knobsSponsoredSee your site on any phone, any day, in any languageReadme
Assura
Write what it should do. AI proves it does.
A contract-first language for the AI era. You write behavioral contracts. AI writes the implementation. An SMT solver proves it correct, or hands you the exact input that breaks it. Ships as Rust.
Details
- Repository
- github.com/assura-lang/assura
- Package
assura- Transport
- STDIO
- Registry
- MCP registry, active