# aare-mcp
MCP (Model Context Protocol) server for [aare-core](https://github.com/aare-ai/aare-core) Z3 SMT verification.
This server exposes aare-core's formal verification capabilities to LLM applications like Claude Desktop and Claude Code.
## Installation
```bash
pip install aare-mcp
```
Or install from source:
```bash
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):
```json
{
"mcpServers": {
"aare-verify": {
"command": "aare-mcp"
}
}
}
```
### Claude Code
Add to your Claude Code MCP configuration:
```json
{
"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:**
```json
{
"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:**
```json
{
"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:**
```json
{
"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:
```bash
export ONTOLOGY_DIR=/path/to/your/ontologies
aare-mcp
```
## Development
```bash
# Install dev dependencies
pip install -e ".[dev]"
# Run tests
pytest
```
## License
MIT
