Guarantee before you estimate

A structural guarantee makes a failure unreachable by construction, through permissions, sandboxes, scaffold rules, or a grammar, so that its probability is a property of the system rather than an estimate from a sample. Guarantee what you can before you estimate, and spend samples only on what construction cannot reach.

What sampling cannot buy#

Sampling is weak evidence about rare harms. Observing a failure that occurs at rate $p$ takes on the order of $1/p$ trials, and estimating $p$ to within about 10% relative error takes on the order of $100/p$ (Kochenderfer et al., 2026). With zero failures in $n$ independent trials, the rule of three bounds the failure rate at about $3/n$ with 95% confidence, so a claim that a catastrophic failure occurs less often than $10^{-6}$ would require millions of representative clean trials if naive sampling were the only evidence. Rare-event assurance develops the bound and the methods that beat uniform sampling.

Suppose SQLAgent, the text-to-SQL agent of Case C, must never issue a destructive write. A clean run of 10,000 tasks bounds that failure rate at about 0.03% ($3/10{,}000$). The calculator starts there, with a target of $10^{-6}$ that takes 2,995,731 clean trials to rule out by sampling alone; drag $n$ to the slider's maximum, a million clean trials, and the bound is still $3.0 \times 10^{-6}$, three times the target.

A read-only credential settles the same question without a single trial, for every path the credential governs. The destructive write becomes unreachable, and $P_f = 0$ holds not as an estimate but as a property of the transition system. The overall shape of rare-event assurance is prevent, search, bound, monitor, and this chapter is about the first word.

Three ways to construct a guarantee#

Formal reachability analysis does not transfer to the learned core of an LLM system, but its concepts do (drawing on Kochenderfer et al., 2026). Three mechanisms turn evaluation problems into guarantees.

Remove the capability#

Capability removal is reachability by construction. Read-only credentials, permission systems, egress allowlists, spend caps, and sandbox boundaries all shrink the set of states the agent can reach, and a safety case should state them as such. The framework files them under structural control, a reachability restriction by construction, and notes that structural controls can dominate statistical monitoring when a property can be guaranteed: they make bad states unreachable rather than merely detectable. SQLAgent's read-only credentials and row-level permissions are one example; Case F's structural permissions, which make unauthorized message destinations unreachable where possible, are another.

Verify the scaffold#

The model cannot be verified, but the orchestration around it is ordinary software over an enumerable action space. Model the agent loop as a transition system whose states record tool availability, permission flags, and pending confirmations; then "no path reaches send_email without passing confirm" is a reachability property you can check exhaustively on the harness. The model chooses which path; the scaffold determines which paths exist. Verify the second; sample the first. The coding agent case uses the idea for approvals: a merge tool that refuses to run without an approval token makes merging before approval unreachable, not rare.

Constrain the output#

Constrained decoding guarantees that every output belongs to a formal language: every emission parses, and every tool call is schema-valid. It is a genuine guarantee, honestly scoped to syntax, never semantics. A schema-valid call to the wrong tool, or with wrong but well-typed arguments, still passes.

Parsers and schema constraints are formal only relative to a syntactic property, never a semantic one, and permissions and sandboxes belong to structural control, the family that prevents failures rather than detecting them (Mechanism families).

The subtraction principle#

Once a property is guaranteed, stop sampling it. This is the subtraction principle: every property enforced by construction or formal verification should be removed from the sampling burden, and scarce empirical eval budget should go to the properties that cannot be guaranteed. For a coding agent, a parser can verify syntax, a type checker types, formal tools memory safety for restricted code, and the scaffold certain authorization invariants, but whether the patch solves the user's real business problem usually remains empirical.

In a safety case the subtraction becomes a partition: every property is either guaranteed by construction, citing the mechanism, or estimated by sampling, citing n and the interval. For Case F's agent, which can send external messages, an illustrative partition looks like this:

A design that checks the confirmation requirement only on the trajectory, rather than enforcing it in the scaffold, detects violations instead of preventing them, so in that design the second row sits on the estimated side. Either way, the calibration labels and trials go to what remains; Case F builds the whole design.

Only as strong as the trusted base#

Every row on the guaranteed side is conditional. A formal guarantee is a property of a configured verification system, not merely an abstract checker. Its configured trusted base includes the permitted axioms, theorem statements, checker version, kernel configuration, and environment assumptions, and whether the optimizer can modify any of them. Optimization pressure does not vanish at a formal check; it moves to those surfaces. The verification hierarchy covers the formal case.

A structural guarantee has a trusted base of the same kind: the credentials and the roles they grant, every connection path to the resource, the allowlist and its version, the sandbox, the scaffold code and the transition model it was verified against, and the grammar. Three questions test it.

• Does it cover every path? A read-only database credential guarantees nothing about a file-export tool or an external API that writes somewhere else. List every route to the unsafe state, not only the obvious one.
• Can the optimizer reach it? If the agent, or the developers tuning it, can edit the permission configuration, the scaffold, or the tests, the guarantee lies inside the modification surface $S$. Keep control and evaluator artifacts outside it; a system that manipulates the process producing its own reward is wireheading.
• Is it the property you need? A guarantee covers the formalized property, not the real-world objective. Read-only SQLAgent cannot drop a table, but it can still return the wrong revenue figure, so correctness stays on the estimated side.

When any part of the trusted base changes, such as a new tool, a new role, or a scaffold release, the guarantee is a new claim and has to be verified again.

From requirement to guarantee or monitor#

One exercise ties these pieces together: write one trajectory requirement as a temporal pattern, name its natural robustness margin, decide whether construction can guarantee it, and, if it must be monitored instead, set a conformal flag threshold from 50 labeled violations. Two illustrative requirements show both branches; Specification covers the patterns and margins in full.

Bounded retries: a guarantee. SQLAgent must resolve or escalate every database error within three retries, the bounded-response pattern $\mathsf{G}\,(\text{error} \rightarrow \mathsf{F}_{\le 3}\,(\text{fixed} \lor \text{escalated}))$. Its natural margin is budget minus usage: the retries left. If the scaffold counts retries and escalates when the third one fails, a violation is unreachable and the property leaves the sampling budget. What remains is to verify that counter on the harness and pin its version.

Policy-compliant messages: a monitor. Whether a message's content complies with policy is semantic, so no permission or grammar can guarantee it, and Case F leaves it to a learned monitor. Its natural margin is the distance between the monitor's badness score and the flag threshold. To bound the miss rate on true violations at level $\alpha$, score $n$ labeled violations and set the threshold at the $\lfloor (n+1)\alpha \rfloor$-th smallest score. With 50 labeled violations and $\alpha = 0.1$, that is the 5th-smallest score, and under exchangeability at most 5/51, about 9.8%, of future true violations score below it. The caveat in one sentence: the bound is marginal rather than per slice, and drift breaks the exchangeability it rests on, so the threshold needs drift detection and recalibration. Monitoring and control in production treats conformal thresholds in full.

In practice#

Build the safety-case partition before you build the sampling plan.

1. List the properties. Take every criterion, and every forbidden action in the agent's action space.
2. Write each as a temporal pattern. Use a safety invariant, precedence, liveness, bounded response, or reachability.
3. Try to make each violation unreachable. Remove the capability, gate it in the scaffold, or constrain the output grammar.
4. Verify the scaffold, not the model. Model the agent loop as a transition system, and check exhaustively that no path reaches the unsafe state.
5. Write down each guarantee's trusted base. Record the configuration it depends on and every path it covers, and confirm that the optimizing loop cannot modify any of it.
6. Subtract. Move guaranteed properties out of the sampling plan, and spend calibration labels and trials on the rest.
7. Monitor or estimate the rest. Use margins, conformal thresholds, and intervals with their n, and rare-event methods where the tail matters.
8. Verify again after every configuration change. A new tool, role, or scaffold release is a new trusted base.

The artifact is a safety-case partition: every property marked either guaranteed, with its mechanism and trusted base, or estimated, with its n and interval.

Common failure modes#

• Sampling what could be guaranteed — a release report counts zero destructive writes in a clean run while the agent still holds write credentials → remove the capability and cite the mechanism instead of the count.
• A guarantee with a side door — the safety case cites a read-only credential, but another tool writes through a different path → enumerate every path to the unsafe state; the guarantee covers only the configured roles and paths.
• Syntax sold as semantics — "every tool call is schema-valid" is offered as evidence that the agent uses its tools correctly → constrained decoding guarantees syntax only; estimate tool-use correctness separately.
• A guarantee inside the modification surface — the agent or its tuning loop can edit the permission file, the scaffold, or the tests → keep control and evaluator artifacts outside what the optimizer can change. See wireheading.

Check yourself#

Analyze. For a tool-using agent you know, separate the guaranteed properties from the estimated ones.

Hint

Start from the action space. For each forbidden action, ask whether a credential, allowlist, cap, sandbox, or scaffold gate removes it; everything else, including every semantic criterion, is estimated.

Evaluate. A vendor's safety case says its agent "cannot exfiltrate customer data" because all outbound traffic passes an egress allowlist. What would you check before accepting the guarantee?

Hint

Check the trusted base: which tools and connection paths the allowlist covers, its version, and who can change it. Then check the property: an allowlist guarantees where data can go, not what is sent there, so data leaving through an approved destination is still on the estimated side.

Create. Take one trajectory requirement from your product, such as "never act without confirmation." Write it as a temporal pattern, name its margin, decide whether construction can guarantee it, and if not, plan a conformal threshold from 50 labeled violations, stating the exchangeability caveat in one sentence.

Hint

For a precedence property, ask whether the scaffold can expose the action only in a confirmed state; if it can, verify that on the harness. If deciding whether the user confirmed needs semantic judgment, the property is monitored, and the threshold follows the $\lfloor (n+1)\alpha \rfloor$ rule.

Further reading#

• Monitoring and control in production — conformal thresholds, alert precision at production base rates, and monitoring versus control.
• Rare-event assurance — the rule of three, importance sampling, and multilevel splitting for what construction cannot reach.
• Mechanism families — where structural control sits among the mechanisms.
• Case F: production safety monitor — the partition applied to an agent that sends messages.
• Kochenderfer et al. (2026), Algorithms for Validation — the reachability, temporal-logic, and robustness vocabulary that this handbook adapts.