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