You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
QWED: deterministic verification for LLMs and AI agents
sidebarTitle
Introduction
description
QWED is a deterministic verification platform for LLMs and AI agents that uses formal methods, symbolic execution, and policy guards to prevent hallucinations.
icon
shield-check
**QWED v6.0.0** is now live — Trust boundary completion: unified `DiagnosticResult` schema across all `/verify/*` endpoints, mandatory control-plane attestation, and deterministic `proof_ref` guarantees. [See what's new →](/changelog#v6-0-0---trust-boundary-completion)
What is QWED?
QWED (Query With Evidence & Determinism) is a trust boundary for AI systems:
LLMs can translate user intent into structured claims.
QWED verifies those claims with deterministic engines before execution or response.
You get proof-backed outcomes instead of probability-only confidence.
QWED is designed for LLM verification, AI agent security, verified tool calls, prompt injection defense, and deterministic transaction verification in high-stakes workflows.
"Do not trust generated output. Verify it."
flowchart LR
U[User Query] --> L[LLM Translation]
L --> Q[QWED Verification]
Q --> R[Verified Result]
L -. Untrusted output .-> X[Possible hallucination]
Q -. Deterministic proof .-> Y[Accepted or rejected]
classDef untrusted fill:#fff4e5,stroke:#f59e0b,color:#92400e;
classDef trusted fill:#ecfeff,stroke:#06b6d4,color:#155e75;
classDef result fill:#ecfdf5,stroke:#22c55e,color:#166534;
class L,X untrusted;
class Q,Y trusted;
class R result;
Loading
Explore common verification problems
Learn how formal verification for LLMs differs from prompting, RAG, and output formatting.
Add pre-execution checks, policy enforcement, and budget controls for agent actions.
Harden your stack against prompt injection, exfiltration, and unsafe execution paths.
Secure Model Context Protocol tools with deterministic verification and tool schema checks.
When to use QWED first
Verify equations, constraints, and logical claims before they reach users.
Catch unsafe patterns, injection risks, and structural errors before execution.
Inspect actions and payloads before external systems are touched.
Add deterministic checkpoints for finance, legal, tax, and regulated systems.
Quick start (5 minutes)
pip install qwed==6.0.0
docker pull qwedai/qwed-verification:6.0.0
# Verify a simple claim
qwed verify "Is 2+2=5?"# -> CORRECTED: The answer is 4# Verify logic constraints
qwed verify-logic "(AND (GT x 5) (LT y 10))"# -> SAT: {x=6, y=9}
Follow [Installation](/getting-started/installation) and set your provider with [LLM configuration](/getting-started/llm-configuration).
Use [Quick start](/getting-started/quickstart) to validate math, logic, code, and SQL.
Use [Integration getting started](/integration/getting-started) and [Production deployment](/integration/production).
Verification engines at a glance
SymPy-based symbolic verification.
Z3 SAT/SMT verification with models.
AST and symbolic checks for risky behavior.
Parser-backed SQL safety and validation.
Type and shape validation for structured outputs.
Data-flow tracking for untrusted inputs.
Explore core, analysis, and specialized engines.
What's new in v6.0.0
All 12/12 sub-issues closed in Epic #263. Every `/verify/*` API pathway returns `DiagnosticResult` and routes through mandatory `enforce_trust_decision`. VERIFIED is a protocol guarantee backed by a non-empty, deterministic `proof_ref`. [Learn more →](/releases)
Observation vs Admission architecture codified: `/verify/*` endpoints return the 3-layer `DiagnosticResult` (`status` / `agent_message` / `developer_fields` / `proof_ref`). [Learn more →](/advanced/diagnostics)
`LogicVerifier` and `FactVerifier` migrated to `DiagnosticResult` with attestation-backed verdicts and advisory checks.
Developer fields snapshotted recursively to prevent alias windows in `enforce_trust_decision`, and `VerificationCache` key namespacing by normalized `tenant_id`.