Skip to main content
Glama
aare-ai

Aare MCP

Official
by aare-ai
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Remote

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 deployed

One endpoint for every MCP toolRayrun runs every MCP server behind one URL and holds the credentials. Each call is decided per client, tool, and argument, then recorded.ray.runAd

Resources

Related MCP Connectors

Appeared in Searches