aare-mcp

MCP (Model Context Protocol) server for aare-core Z3 SMT verification.

This server exposes aare-core's formal verification capabilities to LLM applications like Claude Desktop and Claude Code.

Installation

pip install aare-mcp

Or install from source:

cd aare-mcp pip install -e .

Configuration

Claude Desktop

Add to your Claude Desktop configuration (~/Library/Application Support/Claude/claude_desktop_config.json on macOS):

{ "mcpServers": { "aare-verify": { "command": "aare-mcp" } } }

Claude Code

Add to your Claude Code MCP configuration:

{ "mcpServers": { "aare-verify": { "command": "aare-mcp" } } }

Available Tools

`verify`

Verify LLM output against a compliance ontology using Z3 SMT solver.

Parameters:

llm_output (string, required): The LLM-generated text to verify
ontology (string, required): Name of the ontology to verify against

Example:

verify( llm_output="Based on your income of $75,000 and the property value of $400,000, I recommend a loan amount of $320,000 with an APR of 6.5%.", ontology="mortgage-compliance-v1" )

Response:

{ "verified": true, "ontology": "mortgage-compliance-v1", "violations": [], "parsed_data": { "income": 75000, "property_value": 400000, "loan_amount": 320000, "apr": 6.5 }, "proof": { "method": "Z3 SMT Solver", "version": "4.12.1", "results": [] }, "execution_time_ms": 12 }

`list_ontologies`

List all available compliance ontologies.

Parameters: None

Response:

{ "ontologies": [ "example", "hipaa-v1", "mortgage-compliance-v1" ], "count": 3 }

`parse_claims`

Extract structured data from LLM output using ontology-defined extractors. Useful for debugging.

Parameters:

llm_output (string, required): The LLM-generated text to parse
ontology (string, required): Name of the ontology containing extractor definitions

Response:

{ "ontology": "mortgage-compliance-v1", "parsed_data": { "income": 75000, "loan_amount": 320000 }, "extraction_details": { "income": { "value": 75000, "confidence": 0.95, "source": "75,000", "extractor_type": "money" } } }

Custom Ontologies

Place custom ontology JSON files in the ontologies/ directory or set the ONTOLOGY_DIR environment variable:

export ONTOLOGY_DIR=/path/to/your/ontologies aare-mcp

Development

# Install dev dependencies pip install -e ".[dev]" # Run tests pytest

License

MIT

This server cannot be installed

-

security - not tested

F

license - not found

-

quality - not tested

How are these scores calculated?

Resources

GitHub Repository

Need Help?

Report Issue

Related Servers

Aare MCP

aare-mcp

Installation

Configuration

Claude Desktop

Claude Code

Available Tools

`verify`

`list_ontologies`

`parse_claims`

Custom Ontologies

Development

License

Resources

New MCP Servers

Latest Blog Posts

MCP directory API