Introduction to QWED
QWED (Query With Evidence & Determinism) is a model-agnostic verification protocol for Large Language Models.
Model Agnostic = Your Choice
QWED works with ANY LLM - OpenAI, Anthropic, Gemini, Llama (via Ollama), or any local model. Your LLM, Your Choice, Our Verification.
🌐 Why Model Agnostic?
"Trust, but Verify." — QWED treats LLMs as untrusted translators and uses symbolic engines as trusted verifiers.
QWED is neutral. We verify ALL models equally - no favoritism, no vendor lock-in.
Cost Flexibility
Choose your LLM based on your needs:
| Tier | Monthly Cost | LLM Options | Best For |
|---|---|---|---|
| Local | $0 | Ollama (Llama, Mistral, Phi) | Students, Privacy-focused |
| Budget | ~$5-10 | GPT-4o-mini, Gemini Flash | Startups, Prototypes |
| Premium | ~$50-100 | GPT-4, Claude Opus | Enterprises, Production |
Same verification quality, your choice of cost.
Privacy & Compliance
- Local LLMs = Data never leaves your infrastructure
- Perfect for: Healthcare (HIPAA), Finance (PCI-DSS), Government
- Run on-premise, maintain full control
What is QWED?
QWED (Query-Wise Engine for Determinism) is the verification protocol for AI. It provides deterministic verification of LLM outputs using symbolic engines like Z3, SymPy, and AST analysis.
┌─────────────────────────────────────────────────────────────┐
│ QWED VERIFICATION FLOW │
├─────────────────────────────────────────────────────────────┤
│ │
│ User Query ──▶ LLM (Translator) ──▶ QWED (Verifier) ──▶ ✅ │
│ ↓ (Probabilistic) ↓ (Deterministic) │
│ "2+2=5" "CORRECTED: 4" │
│ │
└─────────────────────────────────────────────────────────────┘
Why QWED?
| Problem | QWED Solution |
|---|---|
| LLMs hallucinate math | Symbolic verification with SymPy |
| LLMs break logic | SAT solving with Z3 |
| LLMs generate unsafe code | AST analysis + pattern detection |
| LLMs produce SQL injection | Query parsing + validation |
Quick Start
# Install the Python SDK
pip install qwed
# Verify math
qwed verify "Is 2+2=5?"
# → ❌ CORRECTED: The answer is 4, not 5.
# Verify logic
qwed verify-logic "(AND (GT x 5) (LT y 10))"
# → ✅ SAT: {x=6, y=9}
Features
- 11 Verification Engines — Math, Logic, Reasoning, Stats, Fact, Graph Fact, Code, SQL, Taint, Image, Schema
- 4 SDKs — Python, TypeScript, Go, Rust
- 3 Framework Integrations — LangChain, LlamaIndex, CrewAI
- Cryptographic Attestations — JWT-based verification proofs
- Agent Verification — Pre-execution checks for AI agents
🆕 What's New in v2.0
| Engine | Upgrade | Impact |
|---|---|---|
| Math | Calculus, Matrix, Finance | 10x more use cases |
| Logic | ForAll/Exists, BitVectors | Formal proofs |
| Code | JS, Java, Go support | 4 languages |
| SQL | Complexity limits | Production-ready |
| Fact | TF-IDF matching | No LLM needed! |
| Graph | NEW! KG Triple Verification | Structured Fact Checking |
| Taint | NEW! Data Flow Analysis | Prevent XSS/RCE |
| Schema | NEW! JSON Math Validation | Invoice/Tax Checks |
| Image | Deterministic size | 100% accurate |
| Consensus | Async + Circuit breaker | Fault-tolerant |
| Stats | Wasm sandbox | Works anywhere |
| Authority | Citation & ISO Checks | Compliance Shield (Phase 9) |