MCP Server

Integrate aare-core Z3 verification directly into Claude Desktop, Claude Code, or any MCP-compatible AI application.

1. What is MCP?

The Model Context Protocol (MCP) is an open standard that allows AI applications to connect to external tools and data sources. With aare-mcp, you can give Claude (or any MCP-compatible LLM) the ability to formally verify its own outputs against compliance rules.

Why MCP? Instead of building verification into your application, Claude can verify its responses in real-time during conversation. This enables self-checking AI that catches compliance violations before they reach users.

2. Installation

From PyPI

pip install aare-mcp

From Source

git clone https://github.com/aare-ai/aare-mcp.git
cd aare-mcp
pip install -e .

Verify Installation

aare-mcp --help

3. Configuration

Claude Desktop

Add the following to your Claude Desktop configuration file: 

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

Claude Code

Add to your project's .claude/mcp.json or global MCP configuration: 

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

With Custom Ontologies Directory

{
  "mcpServers": {
    "aare-verify": {
      "command": "aare-mcp",
      "env": {
        "ONTOLOGY_DIR": "/path/to/your/ontologies"
      }
    }
  }
}

4. Available Tools

The aare-mcp server exposes three tools that Claude can use:

verify

Verify LLM output against a compliance ontology using the Z3 SMT solver. Returns verification result with any constraint violations and formal proof.

llm_output string, required The LLM-generated text to verify
ontology string, required Name of the ontology (e.g., mortgage-compliance-v1)

list_ontologies

List all available compliance ontologies that can be used for verification.

No parameters required.

parse_claims

Extract structured data from LLM output using ontology-defined extractors. Useful for debugging what values will be verified.

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

5. Usage Examples

Verifying a Mortgage Recommendation

When Claude generates a mortgage recommendation, it can verify compliance:

Claude's response (before verification)

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%.

Verification result

{
  "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"
  },
  "execution_time_ms": 12
}

Catching a Violation

Claude's response (with violation)

I can offer you a loan with a DTI ratio of 55% which is quite manageable.

Verification catches the issue

{
  "verified": false,
  "violations": [
    {
      "constraint_id": "MAX_DTI",
      "error_message": "DTI exceeds 43% QM threshold",
      "citation": "12 CFR § 1026.43(c)"
    }
  ],
  "parsed_data": {
    "dti": 55
  }
}

Listing Available Ontologies

Response from list_ontologies

{
  "ontologies": [
    "example",
    "fair-lending-v1",
    "hipaa-v1",
    "mortgage-compliance-v1"
  ],
  "count": 4
}

6. Custom Ontologies

You can add your own ontology JSON files for verification. See the Rule Authoring Guide for how to write ontologies.

Option 1: Environment Variable

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

Option 2: MCP Configuration

{
  "mcpServers": {
    "aare-verify": {
      "command": "aare-mcp",
      "env": {
        "ONTOLOGY_DIR": "./my-ontologies"
      }
    }
  }
}

Ontology File Structure

my-ontologies/
├── my-compliance-v1.json
├── internal-policy-v1.json
└── custom-rules-v1.json

7. Troubleshooting

Tool not appearing in Claude

Check: Restart Claude Desktop after modifying the config file. Verify the config JSON is valid (no trailing commas, proper quotes).

"Ontology not found" error

Check: Run list_ontologies to see available ontologies. Ensure your ONTOLOGY_DIR path is correct and contains valid JSON files.

Verification timeout

Solution: Complex formulas may take longer. The default timeout is 5 seconds per constraint. Simplify your formulas or break them into smaller constraints.

Additional Resources