Guardrails over a whole rule set

The front page shows one puzzle and one check. This page is about the other half of the system: three static analyses that ask questions of an entire rule set at once, each returning a counterexample — the exact input that breaks the property — rather than a bare pass or fail. All three reduce to the same solver primitive how reasoning works describes, asked a different way.

Analysis	Question	Returns
Coverage	Does every input route somewhere?	total, plus a witness input inside any gap
Decision	Can two guards in an ordered table both fire, and can any never fire?	overlapping pairs with the input that fires both; unreachable guard indices
Invariant	Does this transition preserve its obligation?	preserved, plus a violating state when it does not

Both halves of every example below come from one place. The code is quoted directly out of guardrail_calculus.examples.guardrail_analyses, and the result blocks are produced by running that same module's analyses during this site's build — the module tests/examples/test_guardrail_analyses.py pins. Nothing on this page is retyped, so the snippets cannot describe one workflow while the verdicts below them report another, and a solver change that moved any verdict or witness would fail that test rather than quietly rot this page.

Coverage: does every input route somewhere?

A triage workflow routes an insurance claim on two signals — a suspicion score and a claim value:

def coverage_triage_block() -> AgentBlock[Any]:
    """An insurance triage workflow with a genuine hole in it.

    Moderate suspicion (in ``[0.20, 0.75)``) on a claim under £10,000 matches
    none of the three guards -- the gap the coverage analysis finds.
    """
    return (
        agent()
        .given(_.suspicion_score >= probability(0.75))
        .then(_.routes @ routes.to(_triage.fraud_review))
        .given(
            (_.suspicion_score < probability(0.75))
            & (_.claim_value >= money_gbp(10_000))
        )
        .then(_.routes @ routes.to(_triage.underwriter))
        .given(
            (_.suspicion_score < probability(0.20))
            & (_.claim_value < money_gbp(10_000))
        )
        .then(_.routes @ routes.to(_triage.auto_approve))
        .block()
    )

…against a declared input contract, which bounds both signals:

def coverage_domain() -> list[object]:
    """The declared input contract: a suspicion probability and a claim value."""
    return [
        _.suspicion_score >= probability(0.0),
        _.suspicion_score <= probability(1.0),
        _.claim_value >= money_gbp(0),
    ]

Question: does every claim consistent with that domain match at least one of the three guards?

Running workflow_coverage_request(triage, domain) through the coverage analysis:

total  = False
status = UNKNOWN
gap    = { claim_value: 0, suspicion_score: 1/5 }

It is not total. A claim with moderate suspicion (at or above 0.20, below 0.75) and a value under £10,000 matches none of the three guards, and the solver hands back exactly such a claim rather than just the word "no" — the gap above is a real witness, not an illustration. The workflow's own hole, one specific claim wide, found without anyone having to guess it or write a test that happened to hit it.

Decision: can two guards fire at once, or can one never fire?

A second triage table, this time routing on amount and on customer intent:

def decision_triage_block() -> AgentBlock[Any]:
    """A ticket router whose two guards overlap.

    ``amount > £10,000`` and ``intent == "refund"`` are independent conditions,
    so a large refund satisfies both -- the overlap the decision analysis finds.
    """
    return (
        agent()
        .given(_.amount > money_gbp(10_000))
        .then(_.routes @ routes.to(_router.escalate))
        .given(_.intent @ "refund")
        .then(_.routes @ routes.to(_router.billing))
        .block()
    )

Question: can the escalate and billing guards both fire for the same ticket?

overlaps    = guards 0 and 1 co-fire, witness { amount: 10001, intent: "refund" }
unreachable = none

They can. Any refund over £10,000 satisfies amount > £10,000 and has intent equal to "refund" — it matches both guards, and under a first-match ordering one of the two branches silently shadows the other. The decision analysis doesn't resolve which one wins; it surfaces the overlap, with the real witness input above, so the author decides deliberately rather than by accident of rule order.

The same primitive also catches the opposite mistake — a guard that can never fire because an earlier, broader guard already claims every input it would match — reported as an unreachable index rather than an overlap.

Invariant: does this transition preserve its obligation?

The obligation balance >= money_gbp(0), checked against three different preconditions for the same transition:

cases: tuple[tuple[str, list[WireProp]], ...] = (
    (
        "balance >= money_gbp(100)",
        [WireProp(expr=encode(_.balance >= money_gbp(100)))],
    ),
    ("(none)", []),
    (
        "balance <= money_gbp(-1)",
        [WireProp(expr=encode(_.balance <= money_gbp(-1)))],
    ),
)

Precondition	Verdict	Counterexample
balance >= money_gbp(100)	VERIFIED	none
(none)	UNKNOWN	{ balance: -1 }
balance <= money_gbp(-1)	FALSIFIED	{ balance: -1 }

Three different situations, three different verdicts, none of them collapsed into a single pass/fail. The first precondition already entails the obligation. The third makes it impossible outright. The middle row is the one worth sitting with: nothing bounds balance, so the obligation holds for some states and fails for others — a genuine gap the analysis makes visible, with the exact state that breaks it, rather than a false sense of safety from a transition nobody thought to bound.

Why this matters for agent-generated software

In an agent graph, an LLM picks the next node non-deterministically. A guardrail is a separately verified, symbolic layer over the route guards themselves — it proves, independent of what the model chose, that routing stays total (coverage), unambiguous (decision), and state-safe (invariant). When a property fails, the guardrail hands back the exact ticket or state that breaks it, the same way the examples above do.

The aim is not a more trustworthy agent. It is a smaller trusted surface: constraints authored and analysed independently of whatever implementation produces the routing behaviour. Guardrail Calculus does not today check generated code against the model directly — that connection is intent, not a shipped capability — but the three analyses above are real, and they compose with any router, hand-written or generated, that emits the same guard structure.