---
title: "GHSA-mfh5-3c8f-975p"
description: "Logic verification can return VERIFIED for false theorems, non-equivalent formulas and contradictory constraints. Affected and fixed versions of qwed."
url: https://qwedai.com/security/advisories/ghsa-mfh5-3c8f-975p
---

# GHSA-mfh5-3c8f-975p

Logic verification can return VERIFIED for false theorems, non-equivalent formulas and contradictory constraints

## Summary

Two independent root causes let the logic engines produce a `VERIFIED` verdict that does not follow from the input.

### Root cause 1 — Python boolean operators on Z3 objects (`LogicVerifier`)

`src/qwed_new/core/safe_evaluator.py` allows `ast.BoolOp` (`and`/`or`), `ast.UnaryOp(Not)` and multi-operator `ast.Compare`. With Z3 objects, Python evaluates these with `bool()` / structural `==` instead of building a Z3 formula, so the constraint changes silently:

| Call | Result | Correct |
| --- | --- | --- |
| `prove_theorem({"x":"Int"}, [], "not (x == 5)")` | **VERIFIED** "Theorem proved by contradiction" | BLOCKED (counterexample x=5) |
| `check_equivalence({"x":"Int"}, "x == 1 and x == 2", "x == 1")` | **VERIFIED** | BLOCKED (not equivalent) |
| `verify_logic({"x":"Int"}, ["not (x == 1)", "x == 1"])` | **VERIFIED** (SAT) | UNVERIFIABLE (UNSAT) |
| same with `Not(...)` / `And(...)` (control) | correct | — |

Inputs using `or` or chained comparisons raise and fail closed (BLOCKED). The false VERIFIED outcome is specific to `and` / `not`.

Reachable from: the `LogicVerifier` public Python API, and `ConsensusVerifier._verify_with_logic` (constraints produced by an LLM).

### Root cause 2 — DSL compiler auto-creates variables from any string atom (`DSLLogicVerifier`, `/verify/logic`)

`src/qwed_new/core/dsl/compiler.py` L129-134: every `str` node that is not a declared variable becomes `Int(node)`, including quoted literals.

| DSL | Result | Correct |
| --- | --- | --- |
| `(AND (EQ color 1) (EQ color 2))` (control) | UNSAT | — |
| `(AND (EQ color "red") (EQ color "blue"))` | **SAT**, model `color=0, "red"=0, "blue"=0` | UNSAT or BLOCKED |

`/verify/logic` (`src/qwed_new/api/main.py` ~L541) maps SAT to `DiagnosticResult.verified(...)`.

Note: the compiler half of root cause 2 was identified earlier in a related public issue, but the fix at that time changed only `logic_verifier.py`.

## Impact

Downstream components (Finance, Tax, Legal, MCP, A2A, etc.) that gate actions on a logic `VERIFIED` verdict can admit claims that are false. No code execution is involved. This is an integrity violation of the core verification contract ("VERIFIED must follow from the evidence").

## Patches

1.  `SafeEvaluator._validate_ast`: reject `ast.BoolOp`, `ast.UnaryOp` with `ast.Not`, and `ast.Compare` with more than one operator (or rewrite them to `And`/`Or`/`Not` explicitly).
2.  `Z3Compiler._compile_expr`: reject undeclared identifiers and quoted string atoms with a BLOCKED-mapped compile error. Do not auto-create variables.
3.  Regression tests: every row above must not produce VERIFIED.

## Workarounds

Use only `And(...)`, `Or(...)`, `Not(...)` in `LogicVerifier` constraints and avoid quoted literals in DSL. Treat logic VERIFIED verdicts on untrusted input as advisory until upgrading.