aare-core

aare-core

Core verification engine for aare.ai - Z3 SMT solver for LLM compliance verification.

Overview

aare-core provides formal verification (Z3 SMT solver) to validate LLM outputs against structured constraints. The key innovation is the Formula Compiler - constraints are defined entirely in JSON, with no code changes needed.

JSON Formula → Formula Compiler → Z3 Expression → Formal Verification

This is the core library used by all cloud deployments:

• aare-aws - AWS Lambda
• aare-azure - Azure Functions
• aare-gcp - Google Cloud Functions
• aare-watsonx - IBM Cloud Code Engine

Documentation: Rule Authoring Guide | Web Docs

Performance benchmarks: Benchmarks | Web

Installation

# Create a virtual environment (recommended)
python3 -m venv .venv
source .venv/bin/activate  # On Windows: .venv\Scripts\activate

# Core library only
pip install aare-core

# With HTTP server support (quotes required for zsh)
pip install "aare-core[server]"

Quick Start

Command Line (Easiest)

# Verify compliant text (outputs JSON with proof certificate) - this passes
aare-verify --input "Loan approved: 3% rate, DTI 35%, credit score 720" --ontology mortgage-compliance-v1

# Verify non-compliant text - this fails with violation details
aare-verify --input "Approved despite DTI of 55%" --ontology mortgage-compliance-v1

# Verify from a file
aare-verify --file response.txt --ontology hipaa-v1

# Pipe from another command
echo "The loan amount is $350,000 with DTI of 35%" | aare-verify --ontology fair-lending-v1

# List all available ontologies
aare-ontologies

# Compact human-readable output (instead of JSON)
aare-verify --input "..." --ontology mortgage-compliance-v1 --compact

HTTP Server

# Start local server (requires: pip install "aare-core[server]")
aare-serve

# Or with custom port
aare-serve --port 9000

# Test it
curl -X POST http://localhost:8080/verify \
  -H "Content-Type: application/json" \
  -d '{"llm_output": "DTI is 35%", "ontology": "mortgage-compliance-v1"}'

As a Library

from aare_core import FormulaCompiler, LLMParser, SMTVerifier, OntologyLoader

# Load ontology (verification rules)
loader = OntologyLoader()
ontology = loader.load("example")

# Parse LLM output
parser = LLMParser()
data = parser.parse("The value is 50, option A is selected.", ontology)

# Verify against constraints
verifier = SMTVerifier()
result = verifier.verify(data, ontology)

print(result["verified"])  # True or False
print(result["violations"])  # List of constraint violations

With Docker (Self-hosted Server)

# Clone the repository
git clone https://github.com/aare-ai/aare-core.git
cd aare-core

# Start with Docker Compose
docker-compose up -d

# Verify it's running
curl http://localhost:8080/health

Run Server Directly

# Clone and install
git clone https://github.com/aare-ai/aare-core.git
cd aare-core
pip install -e .
pip install flask gunicorn

# Run
python app.py
# or with gunicorn
gunicorn --bind 0.0.0.0:8080 app:app

Architecture

┌───────────────────────────────────────────────────────────────┐
│                      aare.ai Framework                        │
│  ┌─────────────────────────────────────────────────────────┐  │
│  │                    /verify endpoint                     │  │
│  │  ┌──────────┐  ┌──────────┐  ┌────────────────────┐     │  │
│  │  │   LLM    │→ │ Ontology │→ │   Z3 SMT Verifier  │     │  │
│  │  │  Parser  │  │  Loader  │  │  + Formula Compiler│     │  │
│  │  └──────────┘  └──────────┘  └────────────────────┘     │  │
│  └─────────────────────────────────────────────────────────┘  │
│                              ↓                                │
│                    Custom Ontologies ($ONTOLOGY_DIR)          │
└───────────────────────────────────────────────────────────────┘

Formula Compiler

The formula compiler translates JSON constraint definitions into Z3 expressions. This enables:

• No code changes to add new constraints
• Domain-agnostic - works for any verification domain
• Formally verified - mathematically provable correctness

Supported Operators

Formula Examples

// Simple comparison: value ≤ 100
{"<=": ["value", 100]}

// Negation: ¬prohibited
{"==": ["prohibited", false]}

// Implication: condition_a → condition_b
{"implies": [
  {"==": ["condition_a", true]},
  {"==": ["condition_b", true]}
]}

// Disjunction: option_a ∨ option_b
{"or": [
  {"==": ["option_a", true]},
  {"==": ["option_b", true]}
]}

// Complex: (dti ≤ 43) ∨ (compensating_factors ≥ 2)
{"or": [
  {"<=": ["dti", 43]},
  {">=": ["compensating_factors", 2]}
]}

// If-then-else: conditional value
{"ite": [{">": ["score", 700]}, "approved", "denied"]}

// Min/max: fee capped at lesser of $500 or 3% of loan
{"<=": ["fee", {"min": [500, {"*": ["loan", 0.03]}]}]}

API Reference

POST /verify

Verifies LLM output against compliance constraints.

curl -X POST http://localhost:8080/verify \
  -H "Content-Type: application/json" \
  -d '{
    "llm_output": "The value is 50, option A is selected.",
    "ontology": "example"
  }'

Response:

{
  "verified": true,
  "violations": [],
  "warnings": ["Variables defaulted (not found in input): ['variable_name']"],
  "parsed_data": {
    "value": 50,
    "option_a": true
  },
  "ontology": {
    "name": "example",
    "version": "1.0.0",
    "constraints_checked": 5
  },
  "proof": {
    "method": "Z3 SMT Solver",
    "version": "4.12.1"
  },
  "verification_id": "uuid",
  "execution_time_ms": 45,
  "timestamp": "2024-01-01T00:00:00Z"
}

Note: The warnings field appears when variables couldn't be extracted from the LLM output and were defaulted. This helps auditors understand verification scope.

GET /ontologies

List available ontologies.

curl http://localhost:8080/ontologies

GET /ontologies/{name}

Get a specific ontology definition.

curl http://localhost:8080/ontologies/example

GET /health

Health check endpoint.

curl http://localhost:8080/health

GET /verifications (requires persistence)

List recent verification records.

curl http://localhost:8080/verifications?limit=50

GET /verifications/{id} (requires persistence)

Retrieve a specific verification record by ID.

curl http://localhost:8080/verifications/abc-123-uuid

Ontologies

Ontologies (verification rules) are managed separately from the core library. This allows you to update rules without changing the verification engine.

Production ontologies are available in the cloud deployment repositories:

• aare-aws/ontologies

Example ontologies covering common compliance domains:

To use ontologies, set the ONTOLOGY_DIR environment variable:

export ONTOLOGY_DIR=/path/to/your/ontologies
aare-verify --input "Your response" --ontology hipaa-v1

If no ontology is found, an example ontology is used for demonstration purposes.

Creating Custom Ontologies

Create your own verification rules in a custom directory and set ONTOLOGY_DIR to point to it.

Full Documentation: See the comprehensive Rule Authoring Guide for detailed instructions, examples, and best practices. Also available at aare.ai/docs.

Ontology Structure

{
  "name": "my-custom-ontology",
  "version": "1.0.0",
  "description": "Description of your ontology",
  "constraints": [
    {
      "id": "UNIQUE_CONSTRAINT_ID",
      "category": "Category Name",
      "description": "What this constraint checks",
      "formula_readable": "human-readable formula",
      "formula": {"<=": ["value", 100]},
      "variables": [
        {"name": "value", "type": "real"}
      ],
      "error_message": "Error shown when violated",
      "citation": "Reference to regulation/policy"
    }
  ],
  "extractors": {
    "value": {
      "type": "float",
      "pattern": "value[:\\s]*(\\d+(?:\\.\\d+)?)"
    }
  }
}

Variable Types

Extractor Types

Configuration

Environment Variables

Persistence (Audit Trail)

Enable optional persistence to store verification records for audit trails, compliance reporting, and historical analysis.

# SQLite (recommended for single-node deployments)
AARE_PERSISTENCE=sqlite://verifications.db aare-serve

# In-memory (testing only - data lost on restart)
AARE_PERSISTENCE=memory aare-serve

When persistence is enabled:

• Each verification is stored with a certificate_hash (SHA256 of verification metadata)
• The original LLM output is hashed (not stored) for integrity verification
• New endpoints become available: GET /verifications and GET /verifications/{id}
• The /health endpoint includes "persistence": true

Programmatic usage:

from aare_core import SQLiteStore, InMemoryStore
from aare_core.server import create_app

# Use SQLite
store = SQLiteStore("verifications.db")
app = create_app(store=store)

# Or create a custom backend
from aare_core import VerificationStore, VerificationRecord

class PostgresStore(VerificationStore):
    def store(self, record: VerificationRecord) -> str:
        # Store record, return certificate_hash
        ...

    def retrieve(self, verification_id: str) -> VerificationRecord | None:
        # Retrieve by ID
        ...

app = create_app(store=PostgresStore(connection_string))

Docker Compose Configuration

version: '3.8'

services:
  aare:
    image: ghcr.io/aare-ai/aare:latest
    ports:
      - "8080:8080"
    environment:
      - CORS_ORIGINS=https://your-domain.com
      - AARE_PERSISTENCE=sqlite:///data/verifications.db
    volumes:
      - ./ontologies:/app/ontologies:ro
      - ./data:/data
    restart: unless-stopped

Production Deployment

With Nginx (SSL)

server {
    listen 443 ssl;
    server_name api.yourdomain.com;

    ssl_certificate /path/to/cert.pem;
    ssl_certificate_key /path/to/key.pem;

    location / {
        proxy_pass http://localhost:8080;
        proxy_set_header Host $host;
        proxy_set_header X-Real-IP $remote_addr;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
        proxy_set_header X-Forwarded-Proto $scheme;
    }
}

With Kubernetes

apiVersion: apps/v1
kind: Deployment
metadata:
  name: aare-ai
spec:
  replicas: 3
  selector:
    matchLabels:
      app: aare-ai
  template:
    metadata:
      labels:
        app: aare-ai
    spec:
      containers:
      - name: aare-ai
        image: ghcr.io/aare-ai/aare:latest
        ports:
        - containerPort: 8080
        env:
        - name: CORS_ORIGINS
          value: "https://your-domain.com"
        resources:
          requests:
            memory: "512Mi"
            cpu: "250m"
          limits:
            memory: "2Gi"
            cpu: "2"
        livenessProbe:
          httpGet:
            path: /health
            port: 8080
          initialDelaySeconds: 10
          periodSeconds: 30
        readinessProbe:
          httpGet:
            path: /health
            port: 8080
          initialDelaySeconds: 5
          periodSeconds: 10

Integration Example

import requests

def verify_llm_output(llm_response: str, ontology: str = "example") -> dict:
    """Verify LLM output before returning to user"""
    result = requests.post(
        "http://localhost:8080/verify",
        json={
            "llm_output": llm_response,
            "ontology": ontology
        }
    ).json()

    if not result["verified"]:
        raise ComplianceError(
            f"Verification failed: {result['violations']}"
        )

    return result

# Usage
llm_output = my_llm.generate(prompt)
verification = verify_llm_output(llm_output)
if verification["verified"]:
    return llm_output

Performance

aare-core is optimized for high-throughput verification. Benchmarks on Apple M4:

Run the stress test yourself:

python tests/stress_test.py --requests 100 --hipaa-requests 500

The multi-process mode achieves near-linear scaling. Z3 is not thread-safe, so we use separate processes for concurrent workloads.

Full benchmarks: BENCHMARKS.md

Running Tests

pip install -e ".[dev]"
pytest tests/ -v

License

MIT License - see LICENSE for details.

Support

• Documentation: https://aare.ai/about
• Issues: https://github.com/aare-ai/aare-core/issues
• Contact: info@aare.ai