Open-source runtime verification for AI, licensed under Apache-2.0.
QWED
Contact

Type to search pages, engines and advisories.

    Looking for API details?Search the docs

    Evidence

    QWED says it never accepts a claim it cannot prove. Here that is measured. Claims with a known answer run through the proof engines at every release, and the report is published with the release.

    Claims that do not hold, but were accepted

    0

    out of 55 false or unsafe claims in this release’s run. Any number above zero fails QWED’s build.

    • 55 of 55false or unsafe claims caught
    • 29 of 29true claims proved
    • 84claims, across 5 of the 6 proof engines

    By engine

    A true claim that is not proved is held for a person: safe, but incomplete. A false claim that is accepted would be a soundness failure.

    EngineClaimsFalse claims caughtTrue claims provedFalse accepts
    Code1613 of 133 of 30
    Logic1811 of 117 of 70
    Math2412 of 1212 of 120
    Schema107 of 73 of 30
    SQL1612 of 124 of 40

    Past bugs stay fixed

    Each published advisory in which one of these engines returned VERIFIED for a false claim, and whether the claims from it still fail as they should. Every one of them is in the run.

    • GHSA-4phf-6h72-9xfgCodeVerifier certifies command-execution, file-access and exfiltration code as VERIFIED/ADMIT (incomplete fix of GHSA-6rxr-gq43-694g) 3 claims from it in the runStill fixed
    • GHSA-6cpx-8jrq-r7h3SQLVerifier admits credential-dumping and tautology-injection queries (SELECT * bypasses the sensitive-column denylist; tautology check matches exact shapes only) 1 claim from it in the runStill fixed
    • GHSA-6p94-4f75-g2wqSQLVerifier certifies destructive and administrative SQL as VERIFIED/ADMIT (DML hidden in CTEs; incomplete statement-type denylist) 2 claims from it in the runStill fixed
    • GHSA-g25v-44j8-gg7xDSLLogicVerifier NL->DSL bridge returns VERIFIED for contradictory or altered constraints (incomplete fix of GHSA-mfh5-3c8f-975p) 2 claims from it in the runStill fixed
    • GHSA-q5g6-6cw2-cjm3SQLVerifier admits a tautology hidden in a MySQL executable comment, and queries on tables outside the declared schema 3 claims from it in the runStill fixed
    • GHSA-6rxr-gq43-694gCode verifier returns VERIFIED and admits code that runs shell commands 5 claims from it in the runStill fixed
    • GHSA-j622-qffp-rc27verify_math returns VERIFIED for incorrect results on large numbers due to 15-digit evaluation precision 3 claims from it in the runStill fixed
    • GHSA-mfh5-3c8f-975pLogic verification can return VERIFIED for false theorems, non-equivalent formulas and contradictory constraints 3 claims from it in the runStill fixed

    Run it yourself

    No model, network or database is involved: the run calls the engines directly. The cases, the runner and the rules for what counts as accepted are in evals/.

    shell
    git clone https://github.com/QWED-AI/qwed-verification.gitcd qwed-verificationgit checkout c1be8b0dbbcfc875fc0d7996c3ebd6e1f97191f3pip install -e .python -m evals.run

    What this does not measure

    • The translation step

      Turning natural language into a formal statement uses a model, and is not verified.

    • Not in the run yet

      The Symbolic and Stats engines, and the finance, legal, tax and agent packages.

    • Advisory engines

      Fact, Graph, Image, Reasoning and Consensus give signals for review, not proofs.

    • How often a model is right

      This measures QWED’s checks, not the answers a model gives.

    What QWED does not verify