Glossary
The terms QWED uses, each defined once. Other pages, the documentation and the READMEs use them in these senses.
- Deterministic verification
- Checking a claim with a solver, parser or fixed rule, so the same input always gives the same result. No model decides whether the claim holds. Engines
- Fail-closed
- Every outcome other than a completed, positive result stops the action by default, including errors, timeouts, inputs the check cannot handle and cases no rule covers. What fail-closed means for AI checks
- Fail-open
- When a check cannot finish, the action goes ahead as if the check had passed. Reasonable for advice a person will review; risky for actions a system takes on its own. When fail-open is fine
- Verdict
- What a check established about a claim: VERIFIED, UNVERIFIABLE or BLOCKED. It is kept separate from the admission decision.
- VERIFIED
- The claim was proven deterministically, either true or false. It always carries a proof_ref. VERIFIED on its own does not mean allowed.
- UNVERIFIABLE
- The claim could not be proven either way: outside the engines, ambiguous, supported only by a model, or the solver timed out. Never admitted.
- BLOCKED
- The check could not be run at all: the input did not parse, a setting or dependency was missing, or a policy forbids it. Never admitted.
- Admission
- The decision whether the checked output may be acted on: ADMIT or DENY. Only a VERIFIED result whose claim holds is admitted.
- VERIFIED · DENY
- Proven, and what was proven is that the claim is false or unsafe, for example a SQL statement proven to delete data. The proof is the reason it is denied.
- Enforcement
- Acting on the admission decision. QWED returns the decision; the integration, a CI gate or a QWED product such as QWED Security enforces it.
- Formal statement
- The precise version of a claim that an engine can check, such as an equation or a logic formula. QWED verifies the formal statement, not what someone meant by it.
- Untrusted translator
- A language model used only to turn natural language into a formal statement. Its output is treated as untrusted: the translation is not verified, and the formal statement is shown in every result so it can be checked. The translation step
- proof_ref
- A SHA-256 commitment to the evidence behind a VERIFIED result. It makes any later change to the evidence detectable. It is a record of what was checked, not the proof itself.
- Attestation
- A signed token (ES256 JWT) over a result. A signature proves who issued the result and that it was not altered; it does not prove the claim or imply admission. What a signature proves
- Verification Context
- The standard record of a check: what was checked, how, the verdict, the admission decision and the proof_ref. Specification 1.0, in draft. Specifications
- Proof engine
- An engine that can return VERIFIED, always with a proof_ref: Math, Logic, SQL, Code and Schema. Symbolic searches for counterexamples and never returns VERIFIED. Proof engines
- Policy guard
- A check that flags unsafe commands, leaked secrets or untrusted tool calls by rule. Guards deny; they never return VERIFIED. Policy guards
- Advisory engine
- An engine that gives a signal for review, sometimes with a model involved. It never decides; its results are recorded beside the verdict. Advisory engines
- False accept
- A claim that does not hold but was admitted. The one failure fail-closed design cannot catch on its own, so QWED measures it on every release and publishes each case it finds. Evidence