Verification: formal, runtime and consensus

Understand the layered ways a claim or action is confirmed before it is trusted: specification and formal verification of the deterministic wrapper around the model, runtime verification and monitors that check properties as the agent acts, verifiers/judges and consensus (independent re-derivation and N-of-M agreement, with correlated-error limits), and human oversight / autonomy control — and what each layer proves and does not.

Track

Research

Module

11 · Securing & verifying agents

Prerequisites

Evidence, provenance and corroboration

The access and isolation controls of the previous lesson build a deterministic envelope around the model: a validator, a policy engine, an approval gate, an executor. Verification asks how you know that envelope does what it claims for every behaviour the agent might exhibit — including the behaviour of an agent reading adversarial content. The organizing idea is that the model is not verified. It is modelled as a non-deterministic process that may propose anything its interface allows, and the wrapper around it is what gets verified, so that what is proven holds for any concrete agent: today's, the next version's, and the one hijacked by an injection.

Confirmation comes in layers because no single technique covers the whole problem. Formal verification reasons exhaustively about a finite model and says nothing about the running code. Runtime monitors watch the real trace but can only enforce safety, and only for events they observe. Independent verifiers and consensus re-derive a claim but degrade when their errors are correlated. Human oversight catches what no rule specifies but fatigues under volume. Each layer has a precise guarantee and a precise limit, and the engineering is in composing them so the limits do not line up.

To verify formally, you specify properties and check them exhaustively over a finite model. Safety properties say "nothing bad ever happens" and are violated by a finite prefix; liveness properties say "something good eventually happens" and are violated only by an infinite path. For an approval gate, the properties of interest are mostly safety: every payment was approved, every payment matches what was approved, no approval is reused, the budget is never exceeded. These are written as invariants or temporal-logic formulas and checked against a transition system by a model checker, which returns a counterexample — a concrete execution — when one fails.

Wrapper (envelope)

The deterministic components around the model: validator, policy engine, approval gate, executor. This is the object that is verified; the model is left free.

Chaotic model of the agent

The model represented as a process that may take any action its interface permits in each state. Proving a property against it proves it for every concrete agent that acts only through that interface.

Safety vs liveness

Safety: a bad finite prefix exists (counterexample is a finite path). Liveness: only infinite paths violate it (counterexample is a loop), and it needs fairness assumptions about the environment.

Refinement

A mapping showing a concrete design implements an abstract specification, so safety properties of the abstract specification carry down to the design — the bridge from "the policy says" to "the design does".

The payoff of the chaotic model is precise: universal temporal properties (and universal branching properties) that hold for it hold for every concrete agent restricted to the same interface, because a concrete agent's executions are a subset of the chaotic model's. The cost is equally precise. Nothing that depends on what the agent proposes is provable — "the agent never proposes a fraudulent payee" is false in the chaotic model and fails in one step. What is provable is its wrapper form: "a payment to M executes only if the human saw M". Properties with an existential flavour (from any state it is possible to return to idle) are not preserved when you concretize the agent, so they are a warning about engineering liveness, not a security guarantee.

The simplest and most common check is an invariant: a breadth-first search from the initial states visits every reachable state once and tests the predicate; the first state that fails yields a shortest counterexample via its parent pointers. Richer temporal properties use fixed-point labelling or an automaton-product construction, but the shape is the same — explore the reachable state space and report a witness. The dominant cost is state explosion: with several concurrent components the product state space multiplies, and symmetry reduction, partial-order reduction, symbolic representation and bounded checking contain it without eliminating it. This is why formal verification earns its keep on small, critical machines — approval gates, nonce and version handling, circuit-breaker state machines — not on whole systems.

synthetic — invariant check by BFS returning a shortest counterexample
# Checks  G(payment -> approved-and-bound-and-fresh)  on a finite wrapper model.
# The agent is non-deterministic: succ(s) includes EVERY action its interface allows.

def check_invariant(model, holds):
    parent = {}
    queue = deque(model.initial)
    for s in model.initial:
        parent[s] = (None, None)
    while queue:
        s = queue.popleft()
        if not holds(s.labels):             # first violating reachable state
            path = []
            while s is not None:
                s, act = parent[s][0], parent[s][1] if s else None
                ...                          # walk parents to the root
            return False, shortest_path      # a concrete attack nobody had to imagine
        for (s2, act) in model.succ(s):
            if s2 not in parent:
                parent[s2] = (s, act)
                queue.append(s2)
    return True, None                        # holds for ALL behaviours of the model

A verified wrapper guarantees less than its name suggests, and the limits must be stated. You verify a model, not the running code, so a refinement mapping and conformance tests must connect the two. You verify against a specification, which can omit what matters — proving the payment matches the approval says nothing about whether the human approved well. Liveness guarantees rest on fairness assumptions about the environment that the model does not justify. And translating a natural-language requirement into a formula is itself error-prone and must be reviewed. What the model does not cover is exactly what the runtime monitors watch.

Formal verification reasons about a model; production produces a trace. Runtime verification synthesizes a monitor from a specification that reads events as they happen and emits a verdict on each finite prefix. Because a prefix is incomplete, the verdict is three-valued: true if every extension would satisfy the property, false if none would, and inconclusive otherwise. A safety monitor returns false — a bad prefix — the instant a violation occurs; a pure liveness property like "every request is eventually answered" never returns false, because any prefix can still be extended to satisfy it. A classical result establishes the boundary: a mechanism that observes a program's steps and halts it before a violation can enforce exactly the safety properties, never liveness without a deadline. Converting "eventually" into "within D steps" makes it enforceable, at a detection latency equal to the deadline.

Placed at the enforcement point between the agent and the real systems, a monitor is an edit automaton: for each proposed effect it computes the verdict of the extended prefix before the effect occurs, and if the verdict is false it suppresses the event and reacts. If the monitor sees every effect and its verdict is correct, the produced trace satisfies the safety property. Reactions should scale with the certainty of the verdict: a definite safety violation justifies suppression; an expired deadline, whose cause may be benign, justifies escalation; a statistical anomaly justifies asking for review, not blocking. Above these, a circuit breaker opens after repeated alarms and suppresses all effects until a human closes it, and the kill switch — the last rung — must live outside the agent.

synthetic — a two-state safety monitor for "no external send after reading a secret"
# Enforces at the PEP:  G(read_secret -> (not send_external) W task_end)
# Equivalent to a two-state automaton; a safety property, so it is enforceable.

STATE = "clean"   # or "tainted"

def on_event(ev):               # called for EVERY effect before it is produced
    global STATE
    if ev.type == "task_end":
        STATE = "clean"
    elif ev.type == "read_secret":
        STATE = "tainted"
    elif ev.type == "send_external":
        if STATE == "tainted":  # bad prefix detected at the violating event
            return SUPPRESS     # drop the effect; prefix stays legal; raise alarm
    return ALLOW

# The monitor judges what the agent DOES, not what it "intended", so it works
# for any agent. It fails closed: if the monitor is unreachable, no effect passes.

A verifier decides whether a proposed output or action satisfies a property. They differ by the guarantee they give. Exact verifiers (a schema, a code-checked invariant, a policy engine) give a universal guarantee for the property they encode and no other. Executable verifiers (tests, sandboxed execution) give a universal guarantee over the cases executed and nothing outside them. Learned verifiers give, at best, a distributional guarantee with an error rate estimated on a labelled set. A language-model judge asked for a natural-language verdict gives at most a distributional guarantee, with the twist that its input includes text an adversary may control — so it carries the same injection surface as the agent it reviews.

Composition is where intuition misleads. Stacking k independent verifiers multiplies their miss rates, which looks like free security; but independence is the weak assumption. Errors between models are substantially correlated, so a hard case tends to be hard for all of them, and the joint miss rate climbs from the product toward the single worst rate as correlation rises. An N-of-M panel (a jury) reduces missed rejections when its members are genuinely diverse — the Condorcet jury theorem — but the gain stalls under correlation, and five instances of the same model are one vote, not five. Against an adversary the picture is starker: adversarial inputs that transfer across models are a common mode, so a stack of statistical verifiers is no stronger than the set of inputs that fool them all. The guarantee of the chain is the guarantee of its one exact link.

synthetic — N-of-M consensus by independent re-derivation, with a diversity guard
# Re-derive a claim with M verifiers of DIFFERENT families; require N agreeing.
# Independence is asserted and checked, not assumed.

def consensus(claim, verifiers, N):
    assert len({v.family for v in verifiers}) == len(verifiers), \
        "verifiers must be from distinct families (correlated errors erode the gain)"
    votes = [v.recheck(claim) for v in verifiers]     # each re-derives from inputs
    agree = sum(1 for r in votes if r == "accept")
    if agree >= N:
        return "accept"            # confirms the PROPERTY, not that it is wise/safe
    return "escalate"              # a panel may veto or escalate, never authorize

# Reminder on guarantees: if ANY verifier is exact for this property, use it as the
# gate; statistical panels only raise confidence, they do not create a guarantee.

The architectural rule follows. Exact verifiers go first, are cheap, and their rejection is final. Learned verifiers and judges go after, over what passed the exact ones, and their role is asymmetric: they may turn a "yes" into "review", never a "no" into "yes". A judge with veto power but outside the trust boundary is a mere speed bump; a judge that can approve is an attack path, because deceiving it suffices to produce the effect. A learned verdict is one more perception, and perceiving is not authorizing.

Almost every control ends, when it cannot decide, with "escalate to a human". That last link is itself a component with failure modes. A person is in the loop when no action executes without their explicit decision, on the loop when it executes and they supervise with power to override, and out of the loop when they only review afterwards. The choice is made per action and per risk level, not globally. The evidence is blunt: people supervise high-frequency, almost-always-benign streams poorly; complacency and automation bias affect novices and experts alike and are not fixed by training; and acceptance of alerts falls with their number and repetition. An approval is not a control by virtue of existing — it has an error rate that depends on volume, base rate, request design and stakes.

1. 1Classify each proposed action with a deterministic risk function of the canonical intent and state (amount, novelty, reversibility, flow labels, budget) — never let the model set its own level.
2. 2Reserve human attention for the levels that need it: auto-execute within deterministic limits at low risk; notify with an override window; require one or two bound approvals at higher risk; forbid the top level to the agent entirely.
3. 3Derive what the approver sees from the canonical action, and show the model's justification separately, marked as model text, so the person approves fields rather than a persuasive story.
4. 4Bind the approval cryptographically to the exact canonical action (what you see is what you sign), consumed once and before expiry, so changing the action after approval invalidates it.
5. 5Keep the kill switch outside the agent — revoke credentials, drain the executor queue, reach a safe state — so a button the agent can see, delay or reason about is not a stop.

• ▸PROVEN (exhaustively, over the model): a universal temporal property that holds for the chaotic wrapper model holds for every concrete agent restricted to the same interface — including one reading adversarial content.
• ▸PROVEN (operationally): a correct safety monitor at a complete-mediation enforcement point produces a trace satisfying the property; by the enforceability result, this is all a monitor can impose — liveness only with a deadline, at a latency equal to the deadline.
• ▸NOT PROVEN: formal verification checks a model, not the code (needs refinement and conformance tests), and only against the written specification, which may omit what matters.
• ▸NOT PROVEN / eroded: composing statistical verifiers multiplies miss rates only under independence; correlated errors and transferable adversarial inputs collapse the gain to the guarantee of the one exact link.
• ▸NOT PROVEN: a language-model judge gives at most a distributional guarantee and shares the agent's injection surface — it may veto or escalate, never authorize.
• ▸UNKNOWN / human factor: approval quality depends on volume, base rate and design; a logged approval is not evidence of effective oversight, and the model's verbalized reasoning need not reflect what drove its output.

Expected direction: (a) The checker finds: propose(legit) -> request approval -> human approves -> agent changes the proposal to a manipulated payee -> executor pays the current proposal, because it only checked that some approval exists. It exists because "there is an approval" does not bind the approval to the executed action (a time-of-check/time-of-use gap). (b) A monitor at the enforcement point checks each pay event against a safety property like "paid = approved-object" and suppresses the event when they differ; it can enforce this safety property for every observed effect, but cannot enforce liveness without a deadline and does not exist for effects that bypass the enforcement point. (c) A second LLM reviewer gives at most a distributional guarantee, shares the injection surface, and its errors correlate with the agent; a reviewer that can approve becomes an attack path, since deceiving it produces the effect. Fix: bind the approval cryptographically to the exact canonical action, consumed once and before expiry, so changing the action after approval invalidates it; the enabling property is that the approval is bound to (and consumed for) exactly that canonical action.

Why is the model left non-deterministic and only the wrapper verified?

There is no useful finite model of a language model's behaviour and guarantees must hold against adversarial content; modelling the agent as able to propose anything its interface allows means a universal property proven of the wrapper holds for every concrete agent, including a hijacked one. What is provable is the wrapper form of a property, not what the model proposes.

What is the three-valued verdict of a runtime monitor, and which properties can it enforce?

True if every extension satisfies the property, false if none does, inconclusive otherwise. A monitor that suppresses before effect can enforce exactly the safety properties; liveness is only enforceable with a deadline, and then detection latency equals the deadline.

Why does stacking statistical verifiers give less safety than multiplying their miss rates suggests?

Because that multiplication assumes independent errors; model errors are substantially correlated (and adversarial inputs transfer between models), so hard cases are hard for all of them and the joint miss rate climbs toward the single worst rate. Against an adversary the chain is only as strong as its one exact link.

What may a language-model judge do in a secure architecture, and what may it never do?

It may veto or escalate — turn a "yes" into "review". It may never authorize: its guarantee is distributional and it shares the agent's injection surface, so letting a positive verdict alone produce an effect turns deceiving the judge into producing the effect.