Skip to main content
QWED v9.1.0 is the current release. CodeVerifier now admits Python code only when the modules, builtins and special attributes it uses are listed, and each LLM provider runs the model you configure. Some code that earlier releases admitted is now refused, so read the 9.1.0 and 9.0.0 upgrade steps before you upgrade.

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.”

Explore common verification problems

LLM verification

Learn how formal verification for LLMs differs from prompting, RAG, and output formatting.

AI agent security

Add pre-execution checks, policy enforcement, and budget controls for agent actions.

Prompt injection defense

Harden your stack against prompt injection, exfiltration, and unsafe execution paths.

QWED MCP

Give MCP clients access to QWED’s deterministic verification libraries.

When to use QWED first

Math and logic

Verify equations, constraints, and logical claims before they reach users.

Code and SQL

Catch unsafe patterns, injection risks, and structural errors before execution.

Agent tool calls

Inspect actions and payloads before external systems are touched.

High-stakes workflows

Add deterministic checkpoints for finance, legal, tax, and regulated systems.

Quick start (5 minutes)

The examples below use the qwed CLI that this installs. The qwedai/qwed-verification:9.1.0 Docker image runs the API server instead; see Self-hosting.
1

Install and configure

Follow Installation and set your provider with LLM configuration.
2

Run first verification

Use Quick start to validate math, logic, code, and SQL.
3

Integrate into production flow

Verification engines at a glance

Math

SymPy-based symbolic verification.

Logic

Z3 SAT/SMT verification with models.

Code

AST and symbolic checks for risky behavior.

SQL

Parser-backed SQL safety and validation.

Schema

Type and shape validation for structured outputs.

Taint

Data-flow tracking for untrusted inputs.

See all engines

Explore core, analysis, and specialized engines.

What’s new in v9

Allowlist admission for Python code

From v9.1.0, CodeVerifier admits Python code only when every module, module name, builtin and special attribute it uses is on a list, and the code reads no attribute’s value by a name made at run time (hasattr is admitted: it only answers whether an attribute exists, although the lookup can run a property). Each refusal names the module, builtin or attribute. A caller can name modules its own runtime confines with trusted_modules, as the code-execution sandbox does for numpy and pandas; the module checks then skip those modules, so they need that confinement. Read the 9.1.0 notes →
From v9.0.0, QWED names no model of its own: set your provider’s model variable, such as OPENAI_MODEL or ANTHROPIC_MODEL, and pass model= to QWEDLocal, verify() and qwed_sdk.integrations.langchain.QWEDTool. /verify/math runs in worker processes with a time limit, the CSV exports change their columns, and the Go module path moves to /v9. Upgrade every server process together. Read the upgrade steps →
  1. Core concepts
  2. Architecture overview
  3. SDKs overview
  4. API overview
  5. Integration guide