# 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