VERITAS live prover

Formal verification for AI guardrails

Don’t test the guard.
Prove it.

A real prompt-injection guard runs in this tab. Next to it, a SAT solver checks a claim about the guard against all 2256 inputs it can ever see. It finds the way around, closes the hole, and hands you a proof that a standard checker accepts.

Watch it prove

Runs entirely in your browser. Nothing is sent anywhere.

The guard

TRACE · 200 rules · 256 word features
Rules that fired

    The claim

    tap a word to drop it

    2256 is about 1.2 × 1077. Checking one input per nanosecond since the Big Bang would not dent it. The solver reasons about all of them at once.

    The search

    idle

    Every word the guard can see. While the solver works, you are watching its real decisions, slowed down.

    decisions
    0
    conflicts
    0
    learned
    0
    time
    0 ms

    Two questions a test set cannot answer

    Is any word always blocked?

    For each of the 256 words and word pairs, the solver asks: does every prompt that contains it get blocked, whatever else it says?

    Can it block a prompt with no attack words?

    The solver looks for the shortest prompt that the guard blocks while containing none of these attack words:

    How it works

    1. A guard you can read. The TRACE guard is a Tsetlin machine: 200 rules, each an AND of words that must be present or absent. 100 vote unsafe, 100 vote safe, and a prompt is blocked when the unsafe votes win. It scores 84% on the held-out split of deepset/prompt-injections.
    2. Logic, not samples. Each rule becomes a gate and the vote becomes a counter: about 21,000 variables and 48,000 clauses. A claim is true exactly when its negation has no solution.
    3. A solver in a tab. A conflict-driven clause-learning solver, written for this page: watched literals, clause learning, activity-based branching and restarts, in a Web Worker.
    4. Don’t trust it. Check it. Every clause the solver learns is re-derived by unit propagation, independently of the solver. Download the formula and the proof and run drat-trim on them yourself.

    What a proof here does not say

    • It is about words, not meaning. A paraphrase that avoids the words is a different claim, and this small guard misses many of them.
    • A repair has a cost: the new rule blocks every prompt that contains all of its words, harmless ones included. The repair card counts the verdicts it changes on 662 labelled prompts.
    • The guard is small on purpose. Readable models trade accuracy for proofs; the VERITAS paper measures that trade-off. This page reimplements the method in JavaScript on the TRACE guard; the paper’s experiments use the Python package with z3 and PySAT.