Bounded model checking for agent safety#

scripts/cw-check.mjs enumerates every state a GUI agent can reach within k actions of a seeded start state and evaluates a set of policies on each one. It answers a question sampling cannot: not "did 500 rollouts misbehave" but "is there any sequence of at most k clicks that reaches a state where this policy is false".

The output is one of two things per policy. A certificate — the bound was exhausted and no reachable state violates it. Or a counterexample — a literal action sequence, which the tool then replays from a fresh world and re-checks before it will write it down.

node scripts/cw-check.mjs --depth 6 --out site/data/policies.json
node scripts/cw-check.mjs --help
node scripts/cw-check.mjs --self-test      # the evaluator's unit tests

The report is rewritten at every depth boundary. A run stopped part way through therefore still leaves a complete certificate for the last depth it finished, and the report says how much of the next depth it had got through.

Progress, the per-policy verdicts and the termination reason all go to stdout. A run that stops on its budget says so, in the report as well as on the terminal.

What is checked#

The default policy set, buildPolicies() in the script, is fifteen rules about the pull-request review-and-merge flow of http://github.com/northstar/atlas in the company-2026 world — the kind of merge policy a company writes down and then expects a tool to respect. The flow was chosen because it has real business logic behind it: a review has a decision, a merge moves the base ref, a draft is not supposed to be mergeable, and a repository has a writer list.

The agent is alice, who is on that repository's writer list, driving a browser on alice-mac. Nothing about the policies is specific to the checker: they are ordinary Predicate trees with the temporal operators below, and the tool takes whatever set it is given.

What it drives#

The checker uses four things the runtime already exposes, and nothing else.

The scene is the successor generator. A state's enabled actions are the live controls on screen — around thirty-five of them on these pages — not 10⁶ pixels. scene(w, h) returns every node with its role, label, value, disabled flag, bounds, transform, clip and z, before anything is rasterized, so the whole set falls out of one walk over it. The tool keeps the nodes inside the browser window whose role is a real control (button, link, textbox, checkbox, …), groups them by interaction id, and finds a point a click actually reaches each one at by sampling its transformed rectangle and taking the topmost interactive node covering the point. Each control becomes one pointer.v1 click; each text field becomes one edge per value in its abstract domain, a click followed by a keyboard.v1 type.

Reading state is the expensive part. inspect() encodes the whole world — the definition, ninety-three services, five filesystems — as JavaScript objects, and costs about 200 ms. The search needs one repository out of that, tens of thousands of times. exportSnapshot() hands back the same state as one JSON string in about 70 ms, and the repository can be cut out of that string and parsed in well under a millisecond.

That shortcut is held to the exact path. The anchor "github":{ occurs exactly once in the export; if it ever does not, or the object cut out does not have the shape of this repository, the read falls back to inspect() and the report counts it in state_read_fallbacks. Before the search starts, the two reads are compared at the start state and the run aborts if they differ. Every --cross-check states they are compared again and the run aborts if they ever disagree. Counterexample replay uses inspect() alone. --exact-state turns the shortcut off entirely, which is about 2.3× slower and produces the same answers.

The constraint language#

crates/evaluation/src/lib.rs defines Predicate — Equals, Exists, All, Any, Not, evaluated against the inspect() JSON through a JSON Pointer. It is a Rust type with no Wasm or Python binding, so the checker reimplements it in JavaScript, in the shape serde serializes it and with the same semantics: a pointer that does not resolve is not equal to anything (including null), All([]) is true and Any([]) is false, Exists asks only whether the pointer resolves. --self-test covers each of those cases, including the RFC 6901 escape rules and serde's refusal of non-canonical array indices.

Two things are added on top.

Comparison with a margin. Compare {pointer, op, value} with op one of >=, >, <=, <, ==, !=. Beyond holding or not, it returns the signed distance from the boundary, so a near miss is distinguishable from a comfortable pass. A conjunction is as close to the edge as its weakest part and a disjunction as far from it as its strongest, so All takes the minimum margin of its parts and Any the maximum, and Not negates it. ==, !=, Equals and Exists are structural and carry no margin: the tool reports null rather than inventing one. When a structural part is the one that decides a connective — a false conjunct, a true disjunct — the margin of the whole is null too, rather than a number taken from a part that did not decide anything.

Past-time temporal operators, over the prefix of the trajectory ending at the state being evaluated. The interesting properties are temporal: "a refund was never issued unless a manager approved it first" is not a predicate on a final state.

A formula is written in the JSON serde produces for the Rust enum — externally tagged, one key per node — so a policy is data, not code:

{"Never": {"All": [
  {"Compare": {"pointer": "/derived/counts/newly_merged", "op": ">=", "value": 1}},
  {"Not": {"Once": {"Equals": {"pointer": "/derived/events/approved_this_step", "value": true}}}}
]}}

Since is the operator that gets the separation-of-duties policy right. "Whoever approves a pull request does not then merge it" is Since(¬merged_this_step, approved_this_step), and both halves have to be events rather than latches. An agent that merges without ever approving anything does not violate it, because no approval ever started an interval — where Always(nothing_merged) after the first approval would have flagged every merge. And an agent that merges and only afterwards records an approval does not violate it either, because the interval opens at the approval and the merge is behind it — where Since(nothing_merged_yet, approved_this_step) would have flagged that too, on a count that never goes back down.

Margins carry through the temporal operators: Always and Never report the minimum margin over the prefix, Once the maximum, Since the minimum over the interval. The margin a policy carries in the report is the tightest one seen anywhere in the explored graph, not just along one path.

Read a margin as headroom against the policy's own boundary, in whatever the policy counts — margin_unit names it. For a policy of the shape Never(count ≥ 1) over an integer count, the margin is 1 − count: a margin of 1 is an intact policy one event away from the line, and a margin of 0 or less means the line was crossed. The status field, not the sign of the margin, is what says whether the policy held.

What the policies read#

Policies address two roots.

/repo is a raw slice of inspect() — the repository's refs, writers, readers, stars, watchers and pull_requests, exactly as the world reports them. Ordinary JSON Pointers work on it: /repo/pull_requests/15/state.

/derived is a projection computed by project() in the checker. Every field is a pure function of one inspect() result, plus the baseline facts taken at the start state for the fields that describe what changed during the episode. It exists because JSON Pointer cannot count: "at least one approving review from somebody other than the author" is not a path.

The whole inspect() result is deliberately not retained. One evaluation document is kept per state in the search history, and a full inspection is on the order of a hundred megabytes of JavaScript objects.

The abstraction, and why state_hash() is not the key#

state_hash() is full fidelity. It covers the logical tick, the RNG streams, the network log, the response cache and every window coordinate. Two states that differ only in where a window sits hash differently, and the tick alone guarantees that no two states in a run ever collide. Keyed on it, the visited set never collapses anything and breadth-first search degenerates into enumerating every path. It is the right tool for pinning a counterexample's end state down exactly, and the wrong one for deciding that two states are the same state.

The visited set is keyed on a hash of three things.

1. The property-relevant facts — the /derived projection, which is exactly the part of the world the policies can see.
2. The monitor bits — one boolean per temporal subformula of every policy, at the current state. Past-time LTL monitors are finite state, so this is the standard product construction: without it, deduplicating on state alone would be unsound for path-dependent properties, because two paths reaching the same world state can have different histories behind them.
3. The agent-visible interface — which document the browser shows, the sorted set of controls it offers with their roles, labels, values and checked state, and where the keyboard would go. Window position, scroll offsets, ticks, RNG and network bookkeeping are all outside it.

Point 3 is not property-relevant, and including it is a deliberate choice. An abstraction that kept only the property-relevant state would merge "browser on pull request 19" with "browser on the repository home", prune the second the moment the first was seen, and report a certificate for a graph it never walked. Keeping the affordance set means two states are treated as the same state when the policies cannot tell them apart and the same moves are available from both.

That is an abstraction, not a bisimulation. It can in principle merge two states that differ in something neither the policies nor the visible controls expose — clipboard contents, terminal scrollback, a service's state that no page renders. The certificate is therefore over the abstract reachability graph, which is the usual thing a bounded model checker gives you, and the report says so.

Soundness, and what the certificate does not say#

A counterexample is a fact. Every one in the report was produced by the search, then replayed against a world built from scratch — same definition, same seed, same seed script — and re-checked at the end of the replay. A counterexample that does not reproduce is not written out as a violation; the tool prints a refusal and marks the row unverified. The report records the replayed state_hash() so the end state can be reconstructed exactly.

A certificate is narrower than it looks. "P1 holds" means: within the stated depth, over the abstract graph described above, starting from the stated start state, with the stated action space, no reachable state violates P1. It does not mean the property is true in general, and it says nothing at all about a real deployed application. What is verified is the simulation: this world definition, these services, this seed. A policy that holds here holds of a model of the system, which is worth exactly as much as the model.

Three scope decisions narrow it further, and all three are recorded in the output.

• Action space. The controls the browser window paints, and nothing else. The desktop shell around it — dock, wallpaper icons, menu bar, window decorations — is not expanded, and the session is granted no terminal, filesystem or HTTP family, so the agent is a pure GUI browser agent.
• Text entry. Abstracted to a finite domain per field, listed in text_domains in the report. Fields absent from that table take no typed input, which is why the address bar and the search boxes are not part of the action space: typing a URL would make reachability a function of what the tool chose to type rather than of what the pages link to.
• Navigation scope. A state whose document is outside the repository under test is checked for violations but not expanded further. The count is reported as out_of_scope_states.

Partial-order reduction is not implemented, and the report says "partial_order_reduction": false. The runtime makes the independence test unusually easy — fork the state, run a;b and b;a, compare the abstract hashes, and you have tested commutativity rather than over-approximated it — but two things stopped it being worth shipping. It costs two restores, four steps and four state reads per pair, and with around thirty enabled actions per state that is several hundred pairs — more work than simply expanding the state, which costs one state read per successor. And local commutativity on its own does not justify pruning: sound reduction needs the ample-set provisos as well, and an unsound reduction is strictly worse than none. The deduplication on the abstract state is doing the real work anyway; the report's duplicate_states against states_explored shows how much.

Output schema#

site/data/policies.json, one object.

Each policy row:

A counterexample:

Why this works here#

A bounded search needs four things from a simulator, and the engine already had all four: hashable state, so a state seen twice is recognised and not expanded again; a deterministic transition relation, so the same action from the same state always lands in the same place; cheap backtracking, which is what a fork of a checkpoint is; and an enumerable action set, which is what scene() gives — every control on the screen, with its role and its bounds, before a pixel is drawn. A VM or container cannot offer any of them without being rewritten.

The policies are ordinary Predicate trees, the same evaluation surface the agent API exposes for rewards; the actions are ordinary action families, driven through the same step() an agent uses; and the world is the reference company in the world schema. Nothing in the checker is privileged, so a policy set of your own runs the same way.