AI Guardrails That Prove, Not Guess

Combining language models with automated reasoning: rules written in plain English are compiled into formal logic and verified by an SMT solver, enabling decisions to be traced back to an explicit rule rather than a score.

AI guardrails are increasingly used to decide whether a model’s output should be allowed through, blocked, or routed to a human. Most of these guardrails are themselves models: a second LLM scores an answer, spots potential issues, or estimates whether a response is acceptable. That works well for many problems, but it has a structural weakness. The same input can pass on one occasion and fail on another, and the reasoning behind either decision is difficult to inspect.

This article describes a pattern we’ve been investigating, AI+AR: the AI proposes, maps, repairs and explains, while automated reasoning verifies. The language model does what it is good at (reading messy human language) and an SMT solver does what it is good at (evaluating logic exactly).

Scores and proofs

It helps to be precise about what a judge-style guardrail computes. Given an output y, a judge model produces a score g(y) ∈ [0, 1] and the gate applies a threshold:

verdict(y) = pass if g(y) ≥ τ, otherwise block

Everything interesting is hidden inside g. It is a learned function: stochastic under sampling, sensitive to phrasing, and opaque even to its operators. Two runs on the same input can land on opposite sides of τ, and when they do, there is no artefact you can point to that explains why.

Formal methods offer a complementary construction. Instead of asking a model whether something appears acceptable, we compile the rules themselves into logic and ask a sharper question: is this specific claim consistent with these specific rules and facts? The answer is not a score but a verdict with a certificate. Given the same rules and facts, the outcome remains the same.

The mathematics of a verdict

The construction needs three ingredients, all expressed over a shared set of typed variables x₁, …, xₙ (booleans, integers, reals, strings):

1. The policy φ. A quantifier-free formula encoding the rules: boolean connectives (∧, ∨, ¬) over linear arithmetic constraints. This fragment, known as QF_LIA (quantifier-free linear integer arithmetic), is decidable: the solver always terminates with an exact answer.

2. The facts F. A conjunction of ground assignments extracted from the live request, e.g. books_on_loan = 8 ∧ requested_books = 5.

3. The claim c. The proposition the AI’s answer commits to, e.g. “this borrow request is allowed”.

Verification is then two satisfiability queries to the solver, and the pair of results partitions every claim into exactly one of three verdicts:

F ∧ φ ∧ c and F ∧ φ ∧ ¬c (each either SAT or UNSAT)

Proved. If F ∧ φ ∧ ¬c is unsatisfiable, then every model of the facts and rules makes the claim true; in logical notation, F ∧ φ ⊨ c. The claim doesn’t merely avoid contradiction; it is entailed. The response passes.

Refuted. If F ∧ φ ∧ c is unsatisfiable, the claim contradicts the rules. Crucially, the solver returns an unsat core, a minimal subset of conjuncts that cannot hold together, which names the violated rule. The response is held for repair.

Ambiguous. If both queries are satisfiable, the policy genuinely permits both outcomes: the rules are silent on this case. Rather than failing quietly, the system says so and routes the case to review. Under-specification becomes a detectable condition, not a silent coin flip.

Two satisfactory checks partition every claim into exactly one of three verdicts, each mapped to a gate action.

Two properties follow immediately. Determinism: the verdict is a function of the triple (φ, F, c) alone; rerunning the check cannot change the answer. Explainability: a refutation always carries a certificate locating the disagreement in specific, named rules. Neither property is available from a threshold over a learned score.

How it works

The pipeline splits the labour along the line where each technology is trustworthy. Everything probabilistic happens on the AI side of the boundary; everything on the AR side is exact.

The AI+AR pipeline: the language model reads messy human language; the solver evaluates logic exactly

1. Write the rules in plain English. We use a deliberate toy example throughout: “Borrowers need an active library membership, nothing overdue, and at most 10 books out at once.”
2. Compile to formal logic. An LLM extracts typed variables and rules from the text and structures them as machine-verifiable logic, compatible with the CVC5 SMT solver.
3. Store as structured, versioned JSON. Human-readable, diffable, easy to review. Every change bumps the version.
4. Verify real claims against it. When the AI answers a question, the claim and the facts are mapped into the policy’s variables and the solver runs the two satisfiability checks.
5. Gate the response. Proved claims proceed. Refuted claims are held back for repair with the violated rule explicitly named. Ambiguous claims go to review.

A worked example

The library policy compiles to a single formula over four typed variables: m (membership_active, bool), o (has_overdue, bool), b (books_on_loan, int) and r (requested_books, int):

φ ≡ m ∧ ¬o ∧ (b + r ≤ 10)

Consider three requests. In each case the LLM extracts facts from the request, maps them onto the policy’s variables, and the AI’s draft answer supplies the claim c = “the borrow is allowed”.

Three claims against the same policy. In both failures the AI’s answer sounds helpful; the solver locates the exact rule that breaks.

Walk through scenario 2 the way the solver does. The facts are F ≡ (m = ⊤) ∧ (o = ⊥) ∧ (b = 8) ∧ (r = 5). Substituting into φ forces b + r = 13, and 13 ≤ 10 is false in linear integer arithmetic; no assignment can rescue it. Hence F ∧ φ ∧ c is UNSAT, the claim is refuted, and the unsat core is the single constraint b + r ≤ 10. In SMT-LIB, the standard input language of solvers like CVC5, the whole check is a few lines:

(set-logic QF_LIA)
(declare-const membership_active Bool)
(declare-const has_overdue       Bool)
(declare-const books_on_loan     Int)
(declare-const requested_books   Int)

;; policy φ
(assert (and membership_active
             (not has_overdue)
             (<= (+ books_on_loan requested_books) 10)))

;; facts F, extracted from the request
(assert (= membership_active true))
(assert (= has_overdue false))
(assert (= books_on_loan 8))
(assert (= requested_books 5))

(check-sat)   ; => unsat: the claim is refuted

Notice what the two failing scenarios have in common: the AI’s draft answer sounds perfectly helpful. A guardrail scoring tone and topicality could plausibly wave both through. The solver flags them because 8 + 5 = 13 and 13 is not at most 10, and because a lapsed membership makes m false. Small stakes here, but the mechanism is the point: the disagreement is located in a specific rule, not diffused across a score.

What a policy looks like

Policies live as structured JSON: the original English, the typed variables, and the compiled rule, side by side.

{
  "name": "Library Borrowing",
  "original_text": "Borrowing policy
      1. Membership must be active.
      2. No overdue items on the account.
      3. At most 10 books out at once, including this request.",
  "logic": {
    "variables": [
      { "name": "membership_active", "type": "bool",
        "description": "Whether the membership is active" },
      { "name": "has_overdue",       "type": "bool",
        "description": "Whether any items are overdue" },
      { "name": "books_on_loan",     "type": "int",
        "description": "Books currently on loan" },
      { "name": "requested_books",   "type": "int",
        "description": "Books in this request" }
    ],
    "rules": "And(membership_active, Not(has_overdue),
               books_on_loan + requested_books <= 10)"
  },
  "version": 2
}

Three things that earn this format it’s keep:

1. Typed variables. Booleans, integers, reals and strings, each with a description. Types are what let the solver reason exactly instead of approximately.

2. Composable rules. And, Or, Not and comparison operators, evaluated deterministically by CVC5. If a rule is ambiguous, the solver says so explicitly rather than failing silently.

3. Versioning. Every modification increments the version. If someone asks months later why a response was held back, the exact rules that made the call are still there to read.

LLM as a judge vs AI+AR

The most common alternative today is LLM-as-a-judge: a second model reads the first model’s output and scores or critiques it. That is still an LLM reasoning probabilistically about another LLM, so it inherits the same failure modes it is meant to catch.

Where the guarantee stops

It is worth being precise about what is proved. The solver’s verdict is exact relative to the formalisation: if the LLM compiles the English policy into the wrong formula, or maps a request onto the wrong facts, the proof is a correct answer to the wrong question. The trust boundary sits at the two translation steps, which is why the pattern keeps them small, reviewable and versioned. The compiled policy is a diffable artefact a human can audit once, rather than a judgement remade probabilistically on every request.

The ambiguity verdict earns its place here too. A policy that under-specifies a case does not silently default to pass or block; the double SAT check surfaces the gap, which in practice becomes a queue of policy improvements, each one a version bump with a paper trail.

Conclusion

The two approaches are complements, not rivals. LLM-as-a-judge techniques remain the right tool for tone, safety and other properties for which no precise rule exists. Our working hypothesis is simpler: wherever a rule can be written down precisely, a proof is a stronger signal than a judge’s opinion, deterministic where the judge is stochastic and explainable where the judge is opaque.

Whether this pattern becomes a standard component of AI systems remains an open question, but the economics are suggestive: a solver check costs milliseconds, produces a certificate, and never changes its mind.

Ritchie Ng is a Distinguished AI Scientist and CEO Technical Advisor at CommBank, working on applied AI, agentic systems and automated reasoning. He has previously led AI and data science teams across industry and has contributed to research, engineering and education initiatives spanning generative AI, deep learning and large-scale AI systems.

Disclaimer: This article is the opinion of an individual senior technology staff member at the Commonwealth Bank of Australia, and does not represent the views of the Group.