Metadata-Version: 2.4
Name: axiomguard
Version: 0.6.0
Summary: Deterministic Neuro-Symbolic Guardrails for Enterprise AI.
Home-page: https://github.com/witchwasin/AxiomGuard
Author: Witchwasin K.
Author-email: witchwasin <witchwasin@gmail.com>
License-Expression: MIT
Project-URL: Homepage, https://github.com/witchwasin/AxiomGuard
Project-URL: Repository, https://github.com/witchwasin/AxiomGuard
Project-URL: Issues, https://github.com/witchwasin/AxiomGuard/issues
Keywords: ai,hallucination,llm,rag,neuro-symbolic,formal-verification,z3,theorem-prover,smt-solver
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Classifier: Typing :: Typed
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: z3-solver>=4.12.0
Requires-Dist: pydantic>=2.0
Requires-Dist: pyyaml>=6.0
Provides-Extra: anthropic
Requires-Dist: anthropic>=0.39.0; extra == "anthropic"
Provides-Extra: openai
Requires-Dist: openai>=1.0.0; extra == "openai"
Provides-Extra: chroma
Requires-Dist: chromadb>=0.4.0; extra == "chroma"
Provides-Extra: qdrant
Requires-Dist: qdrant-client>=1.7.0; extra == "qdrant"
Provides-Extra: all
Requires-Dist: anthropic>=0.39.0; extra == "all"
Requires-Dist: openai>=1.0.0; extra == "all"
Requires-Dist: chromadb>=0.4.0; extra == "all"
Requires-Dist: qdrant-client>=1.7.0; extra == "all"
Dynamic: author
Dynamic: home-page
Dynamic: license-file
Dynamic: requires-python

  Tests
  Python
  
  Z3

AxiomGuard

  AxiomGuard is not smart. It is correct.

  Deterministic verification engine for LLM outputs.
  Powered by Z3 Theorem Prover. Zero false positives. Fully auditable.
  You write the rules. We enforce them with mathematical proof.

  Philosophy •
  Installation •
  Quickstart •
  Self-Correction •
  LLM Backends •
  API Reference •
  Architecture •
  Contributing

---

## The Pragmatic Enterprise Philosophy

AxiomGuard follows the **"Dumb but Unbreakable"** doctrine. We deliberately reject intelligent verification in favor of mathematically provable, fully auditable, zero-surprise enforcement.

> *"A guardrail that sometimes works is worse than no guardrail at all — it creates false confidence."*

### 1. Deterministic Verification (Math > Vibes)

When Z3 says UNSAT, it's a **mathematical proof** — not an LLM's opinion. Same rules + same claims = same result, every time. No temperature, no randomness, no "it depends."

### 2. Bring Your Own Rules (BYOR)

AxiomGuard is an **enforcement engine**, not a rule generator. Domain experts (compliance officers, doctors, lawyers) write the rules in human-readable YAML. We enforce them. You own the liability — because you wrote the rules, not an AI.

### 3. Transparent Extraction (Auditability First)

The LLM extraction step is the weakest link — and we don't hide it. AxiomGuard always exposes the exact claims the LLM extracted **before** Z3 processes them. Auditors can immediately distinguish extraction errors from logic errors.

### 4. Zero-LLM Debugging (Hardcoded Error Mappings)

Every YAML rule has a `message` field written by a human. When Z3 returns UNSAT, AxiomGuard returns **exactly that string** — no LLM translation, no paraphrasing, no hallucinated explanations.

```yaml
- name: max_transfer_limit
  type: range
  entity: transaction
  relation: amount_thb
  max: 50000
  severity: error
  message: "Transaction exceeds 50,000 THB limit. Requires branch approval."
  #         ↑ This EXACT string is returned on violation. No LLM involved.
```

> Read the full [Architecture Philosophy](docs/architecture_philosophy.md) for the complete rationale and trust model.

---

## Why AxiomGuard?

Standard RAG pipelines retrieve context using **vector similarity** — but vectors encode *similarity*, not *truth*:

```
"The company is in Bangkok"     →  vector A
"The company is in Chiang Mai"  →  vector B

cosine_similarity(A, B) = 0.96  ← Almost identical — but logically contradictory!
```

| Feature | AxiomGuard | Prompt-based checks | Embedding filters |
|---------|:----------:|:-------------------:|:-----------------:|
| **Deterministic** (zero false positives) | Yes | No | No |
| **Auditable** (hardcoded error messages) | Yes | No | No |
| **Self-correcting** (auto-fix hallucinations) | Yes | No | No |
| **Zero token cost** for verification | Yes | No | Yes |
| **Latency** | ~10ms | 500ms+ | ~10ms |
| **Provider-agnostic** | Yes | Varies | N/A |

---

## Installation

```bash
pip install axiomguard
```

With LLM backends:

```bash
pip install "axiomguard[anthropic]"   # Claude
pip install "axiomguard[openai]"      # GPT-4o
pip install "axiomguard[all]"         # Everything + vector DBs
```

### API Key Setup (for full features)

Basic verification (`verify()`) works **without any API key** using the built-in mock backend. For production use (complex sentence extraction, self-correction), set up an LLM backend:

```bash
# macOS / Linux
export ANTHROPIC_API_KEY="sk-ant-..."

# Windows (CMD)
set ANTHROPIC_API_KEY=sk-ant-...

# Windows (PowerShell)
$env:ANTHROPIC_API_KEY="sk-ant-..."
```

> Each user provides their own API key. No keys are bundled with the package.

---

## Quickstart

### 1. Verify a Response (3 lines)

```python
from axiomguard import verify

result = verify("The company is in Chiang Mai", ["The company is in Bangkok"])
print(result.is_hallucinating)  # True
print(result.reason)            # Z3 proved contradiction (UNSAT): ...
```

### 2. YAML Rules + Knowledge Base

Create `company.axiom.yml`:

```yaml
axiomguard: "0.3"
domain: company_facts

entities:
  - name: company
    aliases: ["firm", "org"]

rules:
  - name: hq_location
    type: unique
    entity: company
    relation: location
    value: Bangkok
    severity: error
    message: "HQ is Bangkok — not negotiable."

  - name: ceo_identity
    type: unique
    entity: company
    relation: ceo
    value: Somchai
    severity: error
    message: "CEO is Somchai."
```

```python
from axiomguard import KnowledgeBase, verify_with_kb

kb = KnowledgeBase()
kb.load("company.axiom.yml")
result = verify_with_kb("The CEO is John", kb)

print(result.is_hallucinating)   # True
print(result.violated_rules)     # [{'name': 'ceo_identity', 'message': 'CEO is Somchai.', ...}]
# ↑ The message is EXACTLY what the human wrote in YAML. No LLM translation.
```

### 3. Inspect Extracted Claims (Audit Trail)

```python
from axiomguard import extract_claims

claims = extract_claims("Transfer 800,000 THB to a crypto wallet")
for claim in claims:
    print(f"  {claim.subject}.{claim.relation} = {claim.object}")

# Auditor can verify: Did the LLM extract correctly?
# If it extracted "8000" instead of "800000" — that's an EXTRACTION error,
# not a Z3 error. Transparent. Traceable.
```

### 4. Self-Correction Loop (Auto-Fix Hallucinations)

```python
from axiomguard import KnowledgeBase, generate_with_guard

kb = KnowledgeBase()
kb.load("company.axiom.yml")

result = generate_with_guard(
    prompt="Tell me about the company",
    kb=kb,
    llm_generate=my_llm_function,  # any (str) -> str callable
    max_retries=2,
)

print(result.status)    # "verified" | "corrected" | "failed"
print(result.response)  # The verified (or best-effort) response
print(result.attempts)  # How many tries it took
```

---

## Self-Correction Loop

```
User Prompt + KnowledgeBase
    │
    ▼
┌──────────────┐
│ LLM Generate │  attempt 1
└──────┬───────┘
       │
       ▼
┌──────────────┐
│ Extract Claims│  SRO extraction (auditable)
└──────┬───────┘
       │
       ▼
┌──────────────┐
│ Z3 Verify    │  YAML rules → hardcoded message on failure
└──────┬───────┘
       │
  ┌────┴────┐
  │         │
 SAT      UNSAT
  │         │
  ▼         ▼
DONE   Return hardcoded error_msg
       + build correction prompt
              │
              ▼
         Retry (max 2)
```

**Three-layer fail-safe:** `max_retries` + `timeout_seconds` + optional `max_tokens_budget`.

---

## LLM Backends

AxiomGuard is **provider-agnostic**. The Z3 engine is always the same — only the NL-to-Logic translator changes.

### Anthropic (Claude)

```bash
pip install "axiomguard[anthropic]"
export ANTHROPIC_API_KEY="sk-ant-..."
```

```python
import axiomguard
from axiomguard.backends.anthropic_llm import anthropic_translator

axiomguard.set_llm_backend(anthropic_translator)
result = axiomguard.verify("The company is in Chiang Mai", ["The company is in Bangkok"])
```

### OpenAI (GPT-4o)

```bash
pip install "axiomguard[openai]"
export OPENAI_API_KEY="sk-..."
```

```python
import axiomguard
from axiomguard.backends.openai_llm import openai_translator

axiomguard.set_llm_backend(openai_translator)
```

### Local LLMs (Ollama / vLLM) — No API Key

```python
from axiomguard.backends.generic_http_llm import create_http_translator

axiomguard.set_llm_backend(create_http_translator(model="llama3.1"))
```

---

## API Reference

### Core Verification

| Function | Description |
|----------|-------------|
| `verify(response, axioms)` | Verify against inline axiom strings |
| `verify_with_kb(response, kb)` | Verify against a KnowledgeBase |
| `verify_chunks(chunks, kb)` | Verify & annotate RAG chunks |
| `generate_with_guard(prompt, kb, llm_generate)` | Self-correcting generation loop |
| `extract_claims(text)` | Extract SRO triples (auditable) |

### Data Models

| Class | Description |
|-------|-------------|
| `Claim` | Subject-Relation-Object triple (Pydantic validated) |
| `VerificationResult` | `is_hallucinating`, `reason`, `violated_rules` (hardcoded messages) |
| `CorrectionResult` | `status`, `response`, `attempts`, `history` |
| `KnowledgeBase` | YAML rule loader, compiler & verifier |

---

## Architecture

```
axiomguard/
├── __init__.py              # Public API
├── core.py                  # Orchestration: extraction → resolution → Z3
├── z3_engine.py             # Z3 SMT solver: formal proofs
├── models.py                # Claim, VerificationResult, CorrectionResult
├── knowledge_base.py        # YAML rule compiler & verifier
├── parser.py                # .axiom.yml → Pydantic rule objects
├── correction.py            # Self-correction prompt builder
├── resolver.py              # Entity normalization (deterministic)
├── integration.py           # Vector DB integration (Chroma, Qdrant)
└── backends/
    ├── anthropic_llm.py     # Claude
    ├── openai_llm.py        # GPT-4o
    └── generic_http_llm.py  # Ollama / vLLM / any OpenAI-compatible
```

### Trust Model

```
TRUSTED (deterministic, auditable):
  ├── YAML rules (.axiom.yml)  ← written by human domain experts
  ├── Z3 Solver (math)         ← formal proof, zero false positives
  └── Error messages            ← hardcoded in YAML, no LLM involved

UNTRUSTED (must audit):
  └── LLM extraction            ← always exposed for human review
```

### Design Principles

1. **ML handles language, Math handles truth.** Neither modifies the other.
2. **Zero-LLM-Middleman.** Z3 returns hardcoded messages, not LLM explanations.
3. **BYOR.** We provide the engine. You provide (and own) the rules.
4. **Extraction transparency.** Every claim is visible before Z3 processes it.
5. **Zero false positives.** When Z3 returns UNSAT, the contradiction is *proven*.

---

## Roadmap

- [x] **v0.5.1** — Core engine, self-correction, PyPI, 71 tests
- [ ] **v0.6.0** — Hardened enforcement: deterministic errors, audit trail, date-bounds, negation
- [ ] **v0.7.0** — Advanced rules, Axiom Studio (visual rule editor), LangChain/LlamaIndex
- [ ] **v0.8.0** — Performance: caching, parallel verification
- [ ] **v0.9.0** — Benchmarks against real-world hallucination datasets
- [ ] **v1.0.0** — Production release

See the full **[Roadmap](docs/ROADMAP.md)** and **[Architecture Philosophy](docs/architecture_philosophy.md)**.

---

## Contributing

See **[CONTRIBUTING.md](CONTRIBUTING.md)** for the full guide. Quick start:

```bash
git clone https://github.com/witchwasin/AxiomGuard.git
cd AxiomGuard
pip install -e ".[all,dev]"
pytest tests/
```

---

## Changelog

See **[CHANGELOG.md](CHANGELOG.md)** for the full version history.

---

## License

MIT License. See [LICENSE](LICENSE).

---

  Built by Witchwasin K. (https://github.com/witchwasin) — because AI should prove its answers, not guess them.

