Runtime contracts are the safety case for probabilistic agents

An LLM produces stochastic output. That means you cannot verify its behavior by running it once and checking the result — probabilistic verification at inference time is either infeasible or expensive to the point of defeating cost savings. The answer is not to force determinism on a fundamentally non-deterministic system but to move verification from the model call into contract-based runtime checks at every boundary.

The formal specification research produces a clear architecture: design-by-contract applied to tool calls, sub-agents, and orchestrators. At each boundary, specify preconditions (what must be true before entry), postconditions (what will be true on exit), and invariants (what never changes). This turns every stochastic output point into something that can be verified with a deterministic check — does the output satisfy the postcondition? — rather than an inference-time prediction.

The assume-guarantee composition rule at scale

If agent A produces output that agent B consumes, and both are stochastic, you need more than isolated postconditions. You need a compositional guarantee: "If A produces output satisfying postcondition P_A, then B's preconditions for its next action hold." The assume-guarantee rule from model checking gives exactly this — it says M₁ satisfies A₁→G₁ and M₂ satisfies A₂→G₂, therefore the composition satisfies both. Formally verifiable, in principle.

The gap is tractability. Full state-space exploration for even a two-agent pipeline explodes. The practical solution: verify contract boundaries at deployment time (model-level specification), then check compliance at runtime against observed traces. This produces a three-tier architecture:

1. Offline model-level contracts: verified during deployment/testing, specifying what the model ought to produce
2. Runtime invariant checks: checking postconditions and invariants after each model call, using lightweight deterministic predicates
3. Compositional boundary assertions: validating contract satisfaction at inter-agent boundaries, where output of one is consumed by another

What this looks like in practice

Consider a claims pipeline: an extraction agent reads document text, categorizes the claim type, and passes structured fields to a scoring agent. Each boundary between these three stages is a verification opportunity:

• Extraction → Classification boundary: Did the extracted text match the classification category? Contract: each extracted field must fall within its declared type range (numeric, categorical, or bounded string).
• Classification → Scoring boundary: Does the structured claim data satisfy the scoring model's schema and value constraints?
• Scoring decision → Action boundary: Does the decision fall within the approved action set for this claim type?

Each of these checks is deterministic, fast, and can be enforced at runtime. None require you to "prove" what the model will produce — only to verify that what was produced satisfies the contract.

The boundary between verification and control

There is a subtler issue: verification tells you something violated, but it does not fix it. An enforcement layer sits above verification — policies that reject or requeue outputs failing postconditions, escalate when invariants are breached, or fall back to safer defaults. The specification research calls this design-by-contract with automatic enforcement; the practical distinction is between monitoring (you know things went wrong) and enforcement (the system corrects itself).

The lesson carries up: runtime contracts make stochastic systems verifiable at their boundaries. They do not make every output deterministic — they make every violation detectable and recoverable. That is a safety case for probabilistic agents, without pretending the models are anything other than what they are.