--- title: "Engines" description: "QWED's 13 engines and 9 policy guards, sorted into tiers that decide what each may claim, and the single result shape every check returns." url: https://qwedai.tech/engines --- # Engines Every engine sits in a tier, and the tier decides what the engine is allowed to claim. Only a deterministic proof can make a result verified. - **13** engines - **9** policy guards - **3** results, each with an admission decision ## Three tiers - Tier 1 ### Proof engines Can return VERIFIED Always with a `proof_ref`. All except Symbolic. [6 engines](#proof) - Tier 2 ### Policy guards Block or hold Deterministic rules on inputs, context and tool calls. Never VERIFIED. [9 guards](#guards) - Tier 3 ### Advisory engines Signals for review Heuristic and model-based results are recorded as `advisory_checks`, never as VERIFIED. [5 engines](#advisory) ## Proof engines Symbolic solvers and formal methods. For the claims they cover, an answer either has a reproducible proof or it is not verified. [Math](https://docs.qwedai.com/engines/math) SymPy Arithmetic and algebraic identitiesverifier.py [Guide: can LLMs do maths? How to check AI calculations](https://qwedai.tech/guides/llm-math) [Logic](https://docs.qwedai.com/engines/logic) Z3 Satisfiability of constraints, through the Z3 solver and the QWED DSLlogic\_verifier.py, dsl\_logic\_verifier.py [SQL](https://docs.qwedai.com/engines/sql) SQLGlot Query structure, destructive statements, injection patterns, schemasql\_verifier.py [Guide: checking AI-generated SQL before it runs](https://qwedai.tech/guides/ai-sql) [Code](https://docs.qwedai.com/engines/code) Python AST and rules Dangerous calls and patterns in generated codecode\_verifier.py [Schema](https://docs.qwedai.com/engines/schema) JSON Schema Structure of JSON outputschema\_verifier.py [Guide: validating LLM output with JSON Schema and Pydantic](https://qwedai.tech/guides/llm-json-schema) Symbolic CrossHair (qwed\[symbolic\]) Searches for counterexamples. Returns UNVERIFIABLE or BLOCKED, not proofs.symbolic\_verifier.py The [Stats](https://docs.qwedai.com/engines/stats) engine (stats\_verifier.py) runs statistical code in a sandbox and returns UNVERIFIABLE: running code successfully is not treated as verification. SecureCodeExecutor runs code; it does not verify it. The core counts its engines by module, as listed under each row: 13 in all, because Logic has two. ## Policy guards Deterministic rules applied at runtime. The same input against the same policy always gives the same decision. Guards return block or hold decisions, never VERIFIED. - SystemGuard Shell commands and file paths - ConfigGuard Secrets in configuration - RAGGuard Retrieved context - MCPPoisonGuard MCP tool definitions - ExfiltrationGuard Outbound data - SelfInitiatedCoTGuard Reasoning flow - SovereigntyGuard Data residency and routing - StartupHookGuard Startup hooks - ProcessVerifier Process milestones such as IRAC ## Advisory engines For questions where no formal proof exists. Graph, Image and Consensus can return VERIFIED only on a deterministic sub-path that carries a `proof_ref`. A model fallback never overrides a deterministic result. [Fact](https://docs.qwedai.com/engines/fact) TF-IDF and entity matchingfact\_verifier.py [Graph](https://docs.qwedai.com/engines/graph) Can return VERIFIED on a deterministic sub-pathgraph\_fact\_verifier.py [Image](https://docs.qwedai.com/engines/image) Can return VERIFIED on a deterministic sub-pathimage\_verifier.py [Reasoning](https://docs.qwedai.com/engines/reasoning) Signals for review onlyreasoning\_verifier.py [Consensus](https://docs.qwedai.com/engines/consensus) Can return VERIFIED on a deterministic sub-pathconsensus\_verifier.py ## Every check returns the same shape Since v6.0.0 every engine and guard returns a [`DiagnosticResult`](https://docs.qwedai.com/advanced/diagnostics) with three layers: an `agent_message` that is safe to show an agent, structured `developer_fields` with the evidence, and a `proof_ref`, a hash that binds a VERIFIED result to its proof. DiagnosticResult ``` status VERIFIED | UNVERIFIABLE | BLOCKED agent_message safe for agents, no internals developer_fields structured evidence for developers proof_ref present only when status is VERIFIED ``` - **VERIFIED** Admission: ADMIT or DENY The claim was settled with a proof, and proof\_ref is present. It is admitted only if it holds; a claim proven false or unsafe is denied, with the evidence. - **UNVERIFIABLE** Admission: DENY The claim could not be proven, for example from insufficient evidence, ambiguous input or model-only support. No proof\_ref. Denied by default; a person or your policy can review it. - **BLOCKED** Admission: DENY Verification could not be attempted or completed, for example from a parse error, a missing declaration or a security policy violation. No proof\_ref. Denied. - **Who enforces DENY?** QWED returns the result and the admission decision; it does not stop anything by itself. Your integration enforces DENY, or a QWED product does it for you, as QWED Security does by failing the pull request check. The spec names the admission values ADMIT and DENY. The core library still calls DENY “BLOCKED” in one place; that is [being aligned](https://github.com/QWED-AI/qwed-verification/issues/324). ## Other checks [Taint analysis](https://docs.qwedai.com/engines/taint) follows untrusted input through generated code and flags it before it reaches a sensitive sink such as SQL or a shell. Domain packages such as [qwed-finance](https://finance.qwedai.com) add their own checks on top of these engines. [Full engine reference](https://docs.qwedai.com/engines/overview) [Results at the latest release](https://qwedai.tech/evidence) [What QWED does not verify](https://qwedai.tech/limits) [Install QWED](https://qwedai.tech/install)