A comprehensive guide to writing compliance rules (ontologies) for the
aare.ai /verify API.
An ontology is a JSON file that defines the rules for verifying LLM outputs. It contains:
{
"name": "my-first-ontology",
"version": "1.0.0",
"description": "A simple ontology to verify loan amounts",
"constraints": [
{
"id": "MAX_LOAN",
"category": "Lending",
"description": "Maximum loan amount is $100,000",
"formula_readable": "loan_amount <= 100000",
"formula": {"<=": ["loan_amount", 100000]},
"variables": [
{"name": "loan_amount", "type": "int"}
],
"error_message": "Loan amount exceeds $100,000 maximum",
"citation": "Internal Policy"
}
],
"extractors": {
"loan_amount": {
"type": "int",
"pattern": "\\$([\\d,]+)"
}
}
}
# Using curl
curl -X POST https://api.aare.ai/verify \
-H "Content-Type: application/json" \
-d '{"llm_output": "Approved loan for $75,000", "ontology": "my-first-ontology"}'
| Component | Purpose | Example |
|---|---|---|
| Constraints | Define what must be true | dti <= 43 |
| Variables | Declare data types | {"name": "dti", "type": "real"} |
| Extractors | Pull values from text | Regex pattern to find DTI |
{
"name": "ontology-name",
"version": "1.0.0",
"description": "What this ontology verifies",
"constraints": [...],
"extractors": {...}
}
{
"id": "UNIQUE_IDENTIFIER",
"category": "Category Name",
"description": "Human-readable explanation",
"formula_readable": "x <= 100",
"formula": {"<=": ["x", 100]},
"variables": [
{"name": "x", "type": "int"}
],
"error_message": "Shown when constraint fails",
"citation": "Regulation reference"
}
| Type | Z3 Type | Use For | Example Values |
|---|---|---|---|
bool |
Bool | True/false flags | true, false |
int |
Int | Whole numbers | 600, 100000 |
real |
Real | Decimal numbers | 43.5, 0.05 |
{
"id": "MIN_CREDIT_SCORE",
"formula": {">=": ["credit_score", 600]},
"variables": [{"name": "credit_score", "type": "int"}],
"error_message": "Credit score below 600 minimum"
}
{
"id": "EMPLOYMENT_REQUIRED",
"formula": {"==": ["employment_verified", true]},
"variables": [{"name": "employment_verified", "type": "bool"}],
"error_message": "Employment verification required"
}
{
"formula": {
"and": [
{">=": ["credit_score", 600]},
{"<=": ["dti", 43]}
]
}
}
{
"formula": {
"or": [
{"<=": ["dti", 43]},
{">=": ["compensating_factors", 2]}
]
}
}
{
"id": "DENIAL_REASON_REQUIRED",
"description": "If denied, must provide specific reason",
"formula": {
"implies": [
{"==": ["is_denial", true]},
{"==": ["has_specific_reason", true]}
]
},
"variables": [
{"name": "is_denial", "type": "bool"},
{"name": "has_specific_reason", "type": "bool"}
]
}
| Category | Operators | Example |
|---|---|---|
| Logical | and, or, not, implies, ite |
{"and": [A, B]} |
| Comparison | ==, !=, <, <=, >, >= |
{"<=": ["x", 100]} |
| Arithmetic | +, -, *, /, min, max |
{"+": ["a", "b"]} |
| Constants | true, false, numbers |
{"const": true} |
Extractors pull structured data from unstructured LLM output text.
| Type | Purpose | Key Options |
|---|---|---|
int |
Integer extraction | pattern (regex) |
float |
Decimal extraction | pattern (regex) |
money |
Currency with k/m/b | pattern (regex) |
boolean |
True/false from keywords | keywords, negation_words |
enum |
Predefined choices | choices |
computed |
Derived from other fields | formula |
"credit_score": {
"type": "int",
"pattern": "(?:credit\\s*(?:score)?|fico|score)\\s*(?:is|of|:)?\\s*(\\d{3})"
}
"dti": {
"type": "float",
"pattern": "(?:debt-to-income|dti)(?:\\s*ratio)?\\s*(?:is|of|:)?\\s*([\\d.]+)\\s*%?"
}
"has_documentation": {
"type": "boolean",
"keywords": ["documentation", "paperwork", "documents"],
"negation_words": ["no paperwork", "no documentation"],
"check_negation": true
}
"decision": {
"type": "enum",
"choices": {
"approved": ["approved", "accepted", "granted"],
"denied": ["denied", "rejected", "declined"],
"pending": ["pending", "under review"]
},
"default": "pending"
}
() in your regex
patterns. The first capture group is extracted as the value.
curl -X POST http://localhost:8080/verify \
-H "Content-Type: application/json" \
-d '{
"llm_output": "Approved for $75,000. Credit score: 720, DTI: 35%",
"ontology": "my-ontology"
}'
{
"verified": true,
"violations": [],
"parsed_data": {
"loan_amount": 75000,
"credit_score": 720,
"dti": 35
},
"proof": {
"method": "Z3 SMT Solver",
"version": "4.12.1"
},
"verification_id": "a3d8c1f2-5b7e-4a9d-8c6f-1e2b3a4d5c6e",
"execution_time_ms": 12
}
{
"verified": false,
"violations": [
{
"constraint_id": "MAX_DTI",
"error_message": "DTI exceeds 43% maximum",
"formula": {"<=": ["dti", 43]},
"citation": "12 CFR § 1026.43(c)"
}
],
"parsed_data": {
"dti": 48
}
}
domain-purpose-v1 (e.g., fair-lending-v1)
CATEGORY_DESCRIPTION (e.g., ATR_QM_DTI)
snake_case (e.g., credit_score)
See full production-ready examples on GitHub:
Problem: Extractor couldn't find the value in the text.
Solutions:
Check:
Fix: Add the variable to the
variables array in your constraint.
() is extracted