aare-core 0.1.0

Z3 SMT verification engine for LLM compliance

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

Installation

pip install aare-core

Quick Start

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│     │   │
│  │  └──────────┘  └──────────┘  └────────────────────┘     │   │
│  └─────────────────────────────────────────────────────────┘   │
│                              ↓                                  │
│                    Local Filesystem                             │
│                   (./ontologies/*.json)                         │
└─────────────────────────────────────────────────────────────────┘

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

Category	Operators
Logical	and, or, not, implies, ite (if-then-else)
Comparison	==, !=, <, <=, >, >=
Arithmetic	+, -, *, /, min, max
Constants	true, false, numeric values

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

Creating Custom Ontologies

Create your own verification rules by adding JSON files to the ontologies/ directory.

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

Type	Z3 Type	Use For
bool	Bool	True/false flags
int	Int	Whole numbers
real or float	Real	Decimal numbers

Extractor Types

Type	Description	Example
boolean	True if any keyword found	{"keywords": ["approved", "accepted"]}
int	Extract integer from regex	{"pattern": "score[:\\s]*(\\d+)"}
float	Extract decimal number	{"pattern": "(\\d+\\.\\d+)%"}
money	Extract currency (handles k/m/b)	{"pattern": "\\$([\\d,]+)k?"}
percentage	Extract percentage	{"pattern": "(\\d+(?:\\.\\d+)?)%"}

Configuration

Environment Variables

Variable	Default	Description
PORT	8080	HTTP port
ONTOLOGY_DIR	./ontologies	Directory for custom ontologies
CORS_ORIGINS	https://aare.ai,...	Comma-separated allowed origins
DEBUG	false	Enable debug mode

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
    volumes:
      - ./ontologies:/app/ontologies:ro
    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

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: [e-mail]