Cognitive Fab
Tools Approach Services Blog Get started
Glossary

The words this site uses

Short definitions, in the sense we mean them. Where a term has a broader meaning in the literature, the definition here is the narrower one that the tools actually implement.

stateful code state machine SAM v2 contract invariant reachable state model checking counterexample exhaustive trace corpus mutation adequacy verification gate durable execution effect lethal trifecta fully-mediated reachability reference monitor MCP

The object under test

stateful code
Code whose correctness depends on the order of what came before. An order that can be shipped, refunded and cancelled behaves differently depending on which already happened. Defects in it are combinatorial rather than local: the bug is not on a line, it is in a sequence, which is why reading the diff does not find it.
state machine
A process written down as named situations plus the events that move between them. “Awaiting approval” is a state; “the human approved” is an event. Anything that occupies a situation and moves on events is one, whether or not anybody drew it.
SAM v2
The State-Action-Model pattern the tooling verifies against — second version. Its point for us is separation: a contract declares the actions, states and invariants as data, apart from the implementation, so both can be checked against each other rather than one being trusted.
Used by: polygen, polygraph, polyrun
contract
The declared surface of a machine: which actions exist, which states exist, and the finite domain of data values each action may carry. It is a file, not a comment. Everything the checker explores is bounded by what the contract declares.

What gets checked

invariant
A rule the system must never break, written as a predicate over declared state. “An order is never delivered before it is paid.” Verification means checking invariants against every reachable state rather than sampling the cases somebody thought of.
Elicited by: polynv
reachable state
A configuration the machine can actually get into by some sequence of allowed actions from a starting state. The distinction that matters: a state can be representable in the data and still be unreachable, and a bug in an unreachable state is not a bug.
model checking
Walking every path a state machine can take and testing each rule against all of them, instead of testing only the paths someone wrote a test for. Deterministic: same inputs, same verdict, no model call at check time.
counterexample
The shortest sequence of actions that reaches a state violating an invariant. It is executable, so it is a reproduction rather than a report — and it becomes a regression test on the spot.
exhaustive
Every reachable state over the finite domains the contract declares. That qualifier is the whole meaning: values outside the declared domain are not explored, so the strength of a run is the strength of its declarations.
trace corpus
A set of recorded runs — each a sequence of {pre, action, data, post} — replayed against a machine to check that the code and its contract agree on real history rather than on invented cases.
mutation adequacy
A grade for how strong a set of invariants is, measured by deliberately breaking the machine and counting how many of those broken versions the invariants catch. Rules that catch nothing score nothing, which is the point: it tests the test.
Measured by: polynv

Running it

verification gate
A deterministic pass/fail check in CI or at deploy time. A gate blocks; it does not advise. If it can be overridden by clicking through, it is a report.
Implemented by: polygate
durable execution
Running a machine so that its position survives process death: state is committed after each step, so a restart resumes rather than repeats. Distinct from replay-based durability, which re-runs the code and requires it to be deterministic.
Implemented by: polyrun, and for agents by polyflow
effect
Something the outside world sees — a charge, an email, a Slack post. Kept separate from the transition that decided it, so the decision can be checked before the effect is allowed to happen, and so the same effect is emitted exactly once.

Agents

lethal trifectaSimon Willison
Untrusted input, access to private data, and a way to send data out — all present in one agent session. Each is fine alone. Together they are a leak waiting for a sequence, and no per-call check can see it, because the hazard is the coexistence.
fully-mediated reachability
The design target for an agent guardrail: not “the bad state is unreachable” — over a real agent that is usually unprovable — but that every modeled path into the forbidden region crosses a controllable, default-deny gate.
See: polysec
reference monitorAnderson, 1972
A component every access request must pass through, which cannot be bypassed and is small enough to be checked. It stops a misguided agent — legitimate tools steered by an injection. Containing a compromised runtime that opens its own socket is confinement, a different job.
See: polyman
MCP
Model Context Protocol: the standard way an agent connects to an external tool provider. Relevant here twice — it is how polyflow is mounted, and an over-broad MCP grant is one of the ways a policy quietly permits egress.
Checked by: polycheck