Verification engine tiers: Proof, Policy, Advisory

QWED verification engines are formally classified into three tiers, each with a distinct output guarantee. This classification defines what an engine can and cannot claim, and constrains the “no hallucinations” property to supported proof domains.

The 3-tier engine architecture

A single verification request flows through the tiers: proof engines attempt a deterministic proof, policy enforcement engines apply runtime rules, and advisory engines contribute structured diagnostics. Only a deterministic proof — whether from the proof tier or a deterministic sub-path of a hybrid engine — can produce a VERIFIED status.

As of v6.0.0 every trust-boundary path returns the unified DiagnosticResult model — agent-safe, developer, and proof layers. See the Verification Diagnostics guide for the full model.

Tier 1: Proof engines

Proof engines produce mathematical evidence using symbolic solvers and formal methods. They are the only tier whose entire surface emits VERIFIED, and VERIFIED always requires a proof_ref. (Hybrid advisory engines can also emit VERIFIED, but only on a deterministic sub-path — see Tier 3.) Guarantee. For supported proof domains, hallucinations cannot bypass deterministic verification — an answer either has a reproducible proof or it is not VERIFIED. When to use. Any claim that can be reduced to arithmetic, algebra, a constraint system, an AST invariant, a SQL structure, or a schema check.

Engine	Backend	Domain
Math	SymPy + Decimal	Arithmetic, calculus, matrices, NPV/IRR
Logic	Z3	SAT/SMT, quantifiers, BitVectors
SQL	SQLGlot AST	Query structure, complexity, schema
Code	Multi-language AST	Python, JS, Java, Go security analysis
Schema	Pydantic + Math	JSON structure + embedded calculations
Stats	Pandera + Wasm	Data-frame invariants, sandboxed exec
Symbolic	CrossHair	Reference `DiagnosticResult` engine

Example proof-engine output:

{
  "status": "VERIFIED",
  "engine": "QWED-Math-v2",
  "proof_ref": "sha256:9f2c...",
  "evidence": {"expression": "2+2", "value": 4}
}

Tier 2: Policy enforcement engines

Policy enforcement engines apply deterministic policies to inputs, contexts, and tool calls at runtime. They produce enforcement decisions — BLOCK or UNVERIFIABLE — but never a mathematical proof. Guarantee. Rule-based, reproducible enforcement. The same input against the same policy produces the same decision, with a full decision trace. When to use. Runtime guardrails on agents, MCP tools, RAG contexts, configs, and processes — anywhere you need a deterministic gate but the underlying question is not a math problem.

Engine	Purpose
SystemGuard	System-prompt integrity and policy binding
ConfigGuard	Secret detection and configuration policy
RAGGuard	Retrieval-context injection and poisoning defense
MCPPoisonGuard	MCP tool definition validation
ExfiltrationGuard	Unauthorized data-movement prevention
SelfInitiatedCoTGuard	Reasoning-flow integrity
SovereigntyGuard	Data residency and routing policy
StartupHookGuard	Startup and hook integrity
ProcessVerifier	Milestone-based process validation

Example policy-engine output:

{
  "status": "BLOCK",
  "engine": "ConfigGuard",
  "reason": "SECRETS_DETECTED",
  "decision_trace": ["match:OPENAI_API_KEY@api_key"]
}

Tier 3: Advisory engines

Advisory engines run structured heuristic analysis on inputs where a formal proof is not available. Heuristic and model-based paths emit AdvisoryCheck records only — they can never emit VERIFIED, and their signals are carried as advisory_checks in the diagnostic result. The exception is a deterministic sub-path inside a hybrid engine (Graph or Image), which can emit VERIFIED with a proof_ref; a purely heuristic signal never can. Guarantee. Advisory outputs are transparent and inspectable, but not deterministic proofs. Treat them as inputs to audit and human review, not as verification statuses. An LLM or VLM fallback never overwrites a deterministic verdict. When to use. Fact-similarity checks, knowledge-graph triples, reasoning traces, multi-model consensus, and image analysis — signals that inform a decision but should not gate execution on their own.

Engine	Deterministic path	Advisory-only path
Fact	TF-IDF + entity matching → capped at `UNVERIFIABLE` (heuristic `SUPPORTED` is never `VERIFIED`) or `BLOCKED` (refuted)	LLM fallback → `advisory_checks.llm_reasoning`
Graph	Full-support triple match → `VERIFIED`	NLI fallback → `advisory_checks`
Image	Pixel/metadata evidence → `VERIFIED` with `proof_ref`	VLM cross-check → `UNVERIFIABLE` with advisory checks
Reasoning	—	LLM providers and heuristics are advisory; no provider → `UNVERIFIABLE`
Consensus	Preserves engine-level `BLOCKED` / `UNVERIFIABLE` / `VERIFIED`	Non-unanimous agreement stays advisory

Some engines in this tier are hybrid: a deterministic sub-path (for example, an Image pixel check or a Graph full-triple match) can still emit VERIFIED with a proof_ref or BLOCKED on a refutation. Only the heuristic or model fallback path is strictly advisory. The Fact engine is the exception: its deterministic path is heuristic TF-IDF analysis, so even a SUPPORTED verdict is capped at UNVERIFIABLE. Consensus is a status-preserving aggregator: it never invents a VERIFIED from disagreement, and math-translation failures fail closed. Example advisory-only output (LLM fallback path):

{
  "status": "UNVERIFIABLE",
  "engine": "Fact",
  "advisory_checks": [
    {"name": "tfidf_similarity", "score": 0.62, "threshold": 0.75},
    {"name": "llm_reasoning", "advisory_only": True, "text": "..."}
  ],
  "developer_fields": {"deterministic_confidence": 0.62}
}

Example hybrid deterministic output (Image, claim supported by pixel/metadata evidence):

{
  "status": "VERIFIED",
  "engine": "Image",
  "proof_ref": "sha256:a1b2...",
  "developer_fields": {
    "deterministic_confidence": 0.94,
    "methods_used": [
      {"name": "metadata_extraction", "advisory_only": False},
      {"name": "size_verification", "advisory_only": False}
    ]
  }
}

For comparison, the Fact engine’s deterministic verdict stays capped at UNVERIFIABLE even when a claim is supported — heuristic TF-IDF support is never a proof:

{
  "status": "UNVERIFIABLE",
  "engine": "Fact",
  "constraint_id": "fact_verifier.heuristic_supported",
  "developer_fields": {
    "deterministic_confidence": 0.94,
    "methods_used": [
      {"name": "semantic_similarity", "advisory_only": False},
      {"name": "keyword_overlap", "advisory_only": False}
    ]
  }
}

Behavior by engine type

Compare engines by the output guarantee they provide, not by a single accuracy number — different tiers are answering different questions.

Tier	Emits `VERIFIED`?	Output kind	Determinism	Explainability	Best for
Proof engines	✅ Yes (with `proof_ref`)	Evidence	✅ Reproducible	✅ Full trace + proof	Production AI decisions
Policy enforcement	❌ No — `BLOCK` / `UNVERIFIABLE`	Decision	✅ Reproducible	✅ Decision trace	Runtime agent guards
Advisory (deterministic path)	✅ Yes, only when a deterministic sub-check produces `proof_ref`	Evidence or Analysis	✅ Reproducible	✅ Structured diagnostics	Graph / Image deterministic checks
Advisory (heuristic path)	❌ No — `AdvisoryCheck` only	Analysis	⚠️ Heuristic	✅ Structured diagnostics	Audit and review

For comparison to other approaches:

Approach	Emits proof?	Deterministic	Explainable
QWED proof engines	✅ Yes	✅ Yes	✅ Full trace + `proof_ref`
QWED policy enforcement	❌ No	✅ Yes	✅ Decision trace
QWED advisory	❌ No	⚠️ Heuristic	✅ Structured diagnostics
Fine-tuning / RLHF	❌ No	❌ No	❌ Black box
RAG (retrieval)	❌ No	❌ No	⚠️ Limited
LLM-as-judge	❌ No	❌ No	❌ Prompt-dependent

Engine selection

QWED auto-detects the appropriate engine based on content, then routes through the tiers:

Content pattern	Detected engine	Tier
`2+2=4`, `sqrt(16)`, `derivative`	Math	Proof
`(AND ...)`, `ForAll`, `Exists`	Logic	Proof
`SELECT`, `INSERT`, `DROP`	SQL	Proof
```python, `import`, `function`	Code	Proof
JSON with embedded math	Schema	Proof
Retrieval context	RAGGuard	Policy enforcement
MCP tool definition	MCPPoisonGuard	Policy enforcement
Claim + context	Fact	Advisory
Image bytes + claim	Image	Advisory (hybrid)
Reasoning trace	Reasoning	Advisory
Knowledge-graph triples	Graph	Advisory (hybrid)

Or specify explicitly:

result = client.verify(query, type="math")

Deterministic-first philosophy

Across all tiers, QWED follows a deterministic-first approach:

Try deterministic methods first (100% reproducible).
Fall back to advisory signals only when necessary.
Never promote a heuristic signal to VERIFIED — advisory outputs stay in advisory_checks.

See Determinism guarantee for how to inspect whether a response is SYMBOLIC or HEURISTIC, and the Verification Diagnostics guide for the full DiagnosticResult model.

Engine documentation

Proof engines

Math engine — calculus, matrix, financial
Logic engine — quantifiers, theorem proving
Schema engine — JSON structure and math
Code engine — multi-language security
SQL engine — complexity limits
Stats engine — Pandera invariants, Wasm sandbox
Taint engine — data-flow analysis

Advisory engines

Fact engine — TF-IDF and citations
Graph engine — knowledge-graph triples
Image engine — metadata and VLM cross-check
Reasoning engine — multi-LLM review
Consensus engine — parallel execution

Policy enforcement

Policy enforcement engines ship as SDK guards — see that page for SystemGuard, ConfigGuard, RAGGuard, MCPPoisonGuard, ExfiltrationGuard, SelfInitiatedCoTGuard, SovereigntyGuard, StartupHookGuard, and ProcessVerifier.

Overview

Core Engines

Analysis Engines

Specialized Engines

Verification engine tiers: Proof, Policy, Advisory

The 3-tier engine architecture

Tier 1: Proof engines

Tier 2: Policy enforcement engines

Tier 3: Advisory engines

Behavior by engine type

Engine selection

Deterministic-first philosophy

Engine documentation

Proof engines

Advisory engines

Policy enforcement

​The 3-tier engine architecture

​Tier 1: Proof engines

​Tier 2: Policy enforcement engines

​Tier 3: Advisory engines

​Behavior by engine type

​Engine selection

​Deterministic-first philosophy

​Engine documentation

​Proof engines

​Advisory engines

​Policy enforcement

The 3-tier engine architecture

Tier 1: Proof engines

Tier 2: Policy enforcement engines

Tier 3: Advisory engines

Behavior by engine type

Engine selection

Deterministic-first philosophy

Engine documentation

Proof engines

Advisory engines

Policy enforcement