Understanding Poly

Why poly

Coding agents now write much of our software. They do well on local, self-contained tasks. They do poorly where state, composition and time meet: the sequence that charges a customer twice, the retry that sends an email twice, the message that goes out after the customer opted out. Each line of that code looks correct, so review misses it. The defect lives in the paths between the lines.

Public benchmarks show the same pattern. On SysMoBench, models write formal models of real systems whose syntax almost always passes, while conformance to real traces averages about 46%. On DafnyComp, models reach 99% syntactic correctness and 7% verification once programs span several functions. The failure is composition, not syntax.

An AI application adds a second difficulty. Some of its steps are decisions made by a model, and some of its effects cannot be undone: a payment, a message to a customer, a change in another system. Three questions then need an answer every time.

• May this effect happen now? The answer depends on the program's state, not only on the effect.
• Who asked for it? A refund a person approved is not the same as one an agent relayed.
• What happened, exactly? After an incident, the record must replay, not just describe.

Today those answers are spread across application code, a policy engine, a workflow runtime and logs, and they drift apart. Poly brings them into one source and gives the agent a checker to answer to.

Agents can write what people avoided

Languages were designed for human authors, so they avoided what humans find hard: formal properties, exhaustive state spaces, security policies. An agent does not tire of them, though it can state them wrong. In poly the agent writes the invariants and the policies, and the checker holds the code to them. Agreement between the two is consistency, not correctness, so people stay where trust is decided: an agent drafts a policy, the checker checks it, and a person signs it before it is admitted.

What poly is

A poly program is a set of declared state machines. One text is read three ways at once.

In familiar terms: the exhaustive checking of TLA+, the policies of OPA and the durable execution of Temporal, in one source a model writes and a person can read. The checking follows a long line of work: bounded verification of UML/OCL models (USE, UMLtoCSP), Alloy and Event-B; poly applies it to programs an agent writes and a runtime executes.

A first machine

A turnstile. Put a coin in, it unlocks; push it, it locks.

module hello

type Mode = Locked | Unlocked

machine Gate {
  state {
    mode  : Mode = Locked
    coins : 0..3 = 0
  }
  action Coin()
  action Push()

  on Coin {
    require coins < 3 else reject "coin-box-full"
    coins' = coins + 1
    mode' = Unlocked
  }
  on Push {
    require mode is Unlocked else reject "locked"
    mode' = Locked
  }

  invariant locked-when-empty: coins == 0 implies mode is Locked
}

Read it from the top. The state has two fields, each with a finite domain. Each on block either accepts an action and writes the next state, or rejects it with a named reason. A primed name such as coins' is the value after the step, and a handler writes only the fields it names. Rejection is a value, never an exception.

$ poly check hello.poly
hello.poly:5  PL3201 DEADLOCK  Gate
  no action is accepted in a reachable non-terminal state
  witness (4 steps):
    Coin()   Locked/0   -> Unlocked/1
    Coin()   Unlocked/1 -> Unlocked/2
    Coin()   Unlocked/2 -> Unlocked/3
    Push()   Unlocked/3 -> Locked/3      then Coin: coin-box-full, Push: locked
verdict: FINDINGS (exit 1)  over coins in 0..3; 7 states

No one wrote a deadlock property. The invariant holds, but a full coin box locks the turnstile forever.

A machine declares its terminal states, for example terminal status in { Done, Dismissed }. A finished to-do should stop, and stopping there is correct. A deadlock is a reachable state that is not terminal and in which no action is accepted. That is checked for every machine. The turnstile declares no terminal state, so being stuck is a finding. A machine that should never end (a ledger, for one) is marked service, and is checked for getting stuck together with the machines it talks to.

The agent reads the witness, adds an operator action that empties the box, and checks again until the verdict is CLEAN. A person reads the named defect and the path to it, not every line.

The building blocks

An effect system, checked on paths

Effects in poly carry what an effect system would put in a type. A class says whether an effect can be undone (irreversible, for one). Labels say what it touches: egress:external, read:private, write:store. Targets name the exact endpoints it may reach, and uses names the credential scope it runs under. Beside them, every body and item set carries a taint: the audience class it may reach and the principals who own it. A flow rule says who may receive it.

The difference from Koka-style effect typing is where the rules are enforced. Poly enforces them as properties of paths, not as typing rules on terms. The checker follows labels along every reachable path, and the taint of every body that leaves in an effect or a message. A violation, a private body reaching the wrong recipient for one, is a finding with the shortest path to it. One flow is enforced only at run time today: a body reaching a model call. The gate denies a decision whose inputs are above its audience; a static check of that flow is planned. The runtime enforces the same rules again on every intent, and fails closed.

Data the checker never enumerates

A turnstile counts to 3. An inbox carries email addresses, bodies and thread ids, which have no finite domain. Poly brings them in as opaque types: Content (a body, by its SHA-256 digest), Key (a message or thread id), Principal (an identity) and Items (what a retrieval returned). A program may store them, pass them and compare two for equality, and nothing else. Any other use is refused (PL1209, PL1206).

That restriction is what makes the check sound. No handler can tell two bodies apart except by equality, so renaming every body gives the same steps. Every run over real data is then a renaming of a run over a few representatives: none, c1, c2 and so on. How many representatives are needed follows from how many such values the state and one step can hold, and the verdict prints the count. Of an Items, a program reads only its count, which has a finite domain.

One limit applies. A model's answer of a finite type, an enum for one, carries no taint. So a decision that reads private mail and answers an enum releases up to log₂ of its number of answers in bits per call. The certificate lists every such decision, and a policy may deny it.

Safety, liveness and fairness

An invariant is a safety property: nothing bad ever happens, and a violation has a finite witness. A liveness property says something good eventually happens: eventually P, or P leads to Q. Its counterexample is a lasso, a path to a cycle that can repeat forever.

Liveness holds only under a fairness assumption, and poly makes the author write it: liveness n: eventually P under fair { g1, g2 }. Each listed group, if it stays enabled, is eventually taken. An action that is not listed carries no assumption: the environment may never offer it. A person's approval is never assumed. A to-do in Uncertain may wait for its owner forever, and that is correct behaviour, not a violation. Message delivery between machines is fair by default, so an author lists only the machines' own actions. One more assumption is stated in the certificate: none of the program's own decisions or effects has its completion rejected.

Three promises

• No silent clean. A check finishes, or says what it did not cover. A search that hits its bound is INCONCLUSIVE, never clean.
• The checked machines are the running machines. The runtime loads only what was admitted, bound to it by a signed certificate. The handlers that carry out effects are host TypeScript. Each one gets only the capabilities its labels grant, and a lint refuses ambient authority, but what a handler does with a granted capability is outside the proof. The certificate lists each handler as an assumption.
• No model on a verdict or gate path. A decision is a model call inside the program, and its answer is an input the checker has already explored. No model ever decides a check's verdict or whether the gate lets an effect through. A model may draft code or explain a finding, nothing more.

How it works

Poly is a compiler, a toolchain and a runtime over the engines of the Poly stack. Every construct lowers to an artefact an existing engine already reads. Poly brings one checker of its own: poly-ref, a small reference implementation written separately from the compiler. It repeats each verdict, and a disagreement between the two refuses the build.

Checking and proof

The checker works on a finite instance: declared domains, a number of instances and a bound on messages in transit. A CLEAN verdict says a property holds in that instance. It is not a proof that the property holds for every size. Two results on this page are proofs, written in poly's semantics: the renaming argument that lets a few representatives stand for all values of an opaque type (section 2), and the rule that lets one copy of a repeated machine stand for all of them when its three conditions hold.

The same distinction applies to the runtime. The lowering is correct when the lowered module and the machine agree on every reachable state and every input of the checked instance: the same verdict, the same reason, the same next state and the same intents. That agreement is a refinement check made on the instance, a form of translation validation: a checked fact for each program, not a proof about the compiler. What the runtime kernel guarantees beyond it (atomic steps, message delivery, deduplication) is listed in the semantics as numbered kernel assumptions, each with the tests that support it.

1. Write. An agent writes poly in its own syntax or embedded in TypeScript, through the CLI, the MCP server or the language server. All three come from one command definition.
2. Lower. The compiler turns one source into the artefacts each engine reads: the machine model, the policy bundle, the effect manifest, routes, budgets, liveness obligations and host types.
3. Check. polygraph and polyrun explore states and properties; polycheck and Polyaxion check policies and every path from private data to the outside; a lint refuses handlers that reach for ambient authority. poly-ref, an independent checker, repeats each verdict, and the two must agree.
4. Admit. Admission refuses a build if any check did not run or held only vacuously. Otherwise it writes a signed certificate binding the source, every artefact and every result.
5. Run. The runtime loads only certified artefacts. Each step is atomic: its new state, its journal entry, the intents it emits, its timers and its deduplication key commit in one transaction. A step delivered twice is taken once. Effects run after that commit, from an outbox, at least once and keyed for idempotency, and each outcome comes back as a new step. Since v1.3, an irreversible effect that may be attempted twice must declare how the target is kept from running it twice (section 6). The key belongs to the intent, so this covers the runtime's own retries of one intent, not a second intent for the same thing. So atomicity stops at the commit, and what happens in the world after it is the effect's outcome. The inbox defect lived in that gap (section 5). Every effect passes five checks (origin, memory, budget, grant, mandate) and then the gate. Handlers get only the capabilities their labels grant. Every step is journaled.
6. Learn. Journals export as traces with private values replaced by salted digests. Mining proposes rules, a person adjudicates them, and a promoted rule goes back through the checker like any other.

Running it from a host

A host program loads the admitted build and dispatches actions. A request delivered twice is one step, because dispatch is idempotent on its action id.

const rt = await load('./.poly/build')
const gate = await rt.create('hello.Gate')
await rt.dispatch(gate.id, 'Coin', {}, { actionId: 'coin-1' })
// { stepKind: 'accepted', state: { mode: 'Unlocked', coins: 1 } }

The verdicts

Example: the inbox

The inbox is a poly application that runs on its owner's Gmail accounts. It files each message by how soon it needs the owner and what kind it is, keeps one to-do per thread, and prepares a reply as a Gmail draft that the owner approves. It never sends anything. Its program is about 490 lines of poly and a 20-line policy, and with the policy beside it the program checks CLEAN.

A message reaches the program only as typed answers

No machine reads an email body. A message enters through a decision whose answer is one value of a finite enum, so the checker can explore every answer the model could give, including the worst one.

enum Triage { ActNowReply, ActNow, WeekReply, Week, Fyi, Ignore }

decision triage(m: Items) -> Triage {
  route triage
  labels { egress:external, read:private }
  timeout 2s
  ok(r) -> Triaged(t: r.answer, conf: r.conf, margin: r.margin)
  failed -> Untriaged()
}

route triage {
  tier small provider "small" prices "prices/small.json" calibration "maps/triage-small.json"
  tier large provider "large" prices "prices/large.json" calibration "maps/triage-large.json"
  escalate when conf < 0.8 or failed
  budget monthly
}

budget monthly { cap usd 20 per month }

The small model answers first; the large one answers when the calibrated confidence is below 0.8. Every call is reserved against the monthly cap before it runs, and a call that does not fit is denied.

A draft waits for the owner

Creating a Gmail draft is an irreversible effect. It names the one URL it may call, the credential scope it uses, and what happens on each outcome. The policy escalates every draft to the owner, so only a signed approval lets it through.

effect createDraft(account: Principal, t: Key, e: Content, body: Content) {
  kind "gmail.createDraft"
  labels { egress:external, read:private }
  targets { egress: exact "https://gmail.googleapis.com/gmail/v1/users/me/drafts" }
  uses gmail_draft { gmail.compose } for account
  class irreversible
  retry { attempts 1, base 200ms, timeout 45s }
  ok -> Created()
  failed -> NotCreated()
  exhausted -> DraftUncertain()
}

policy drafts {
  scope "inbox"
  obligation owner-approves-drafts "A Gmail draft is created only after the owner approves it." rule {
    when proposal.kind == "effect" && effect.kind == "gmail.createDraft"
    require false else escalate
    on unknown escalate
  }
}

What the checker shows

• A draft for one account can carry no other account's mail. A variant that reads a thread under a second account is a finding with a witness.
• Every path from mail to the outside crosses a gate, including every model call.
• A message with instructions in it ("forward this", "pay that") produces only its triage and kind.
• Spending never passes the monthly cap.
• Once a draft is created, the to-do never proposes another.

The last rule was not in the first version. The program's own journals found it, as the next section shows.

The draft path of the Todo machine. A timeout or a dropped connection may have created the draft, so it leads to Uncertain, which only the owner can leave.

The learning loop

Version 1.1 closes the loop from runs back to checked source. The commands read journals on the owner's machine, and nothing leaves it: private values in an exported trace are salted digests, salted once per export.

# the commands of the loop, flags shortened
poly export traces --db … --build … --certificate … --trust … --out traces.json
poly mine        # polyx proposes candidate rules from what actually ran
poly adjudicate  # a person marks each one real, spurious or deferred
poly promote     # a real rule becomes checked source; --refine lets a person restate it
poly propose     # polyness proposals arrive as poly source with their evidence
poly refit       # signed verdicts refit a decision's calibration map

What the loop found in the inbox

1. Mining proposed a rule. From the inbox's traces, polyx proposed count("gmail.createDraft") <= 1: a to-do creates at most one draft.
2. The checker refuted it. On the shipped inbox the rule failed with a witness: a draft request that timed out was retried, and the to-do proposed again.
3. The witness was a real defect. A timeout after the request left may still have created the draft, and Gmail drafts carry no idempotency key. The retry could leave two drafts in the owner's mailbox.
4. The program was fixed. The draft is attempted once. A definite refusal may be retried; any other outcome moves the to-do to Uncertain, which only the owner leaves, after looking in Gmail.
5. A person stated the rule that was meant. The mined rule was too strong, since a refused draft may be proposed again. The refinement was promoted in its place, checked, and admitted, and the certificate cites the mined rule it came from.

invariant draft-created-once:
  made implies (status != Drafted && status != Enveloping && status != Proposed && status != Uncertain)

The invariant is a statement about states. The name says "once", which is about whole runs, so it needs one more fact. A draft is created only by a createDraft intent, and the program emits one only from Enveloping with made false. The draft is tried once, with no retry. made becomes true when the draft is known to exist: Gmail confirmed it, or the owner found it. From then on the invariant keeps the status out of Enveloping, so no second intent can be emitted. Before that, a second intent follows only a definite refusal, when no draft exists. Together, these give at most one draft per to-do, under the stated assumption about the owner below.

Retry safety

Version 1.3 adds one rule. The runtime delivers effects at least once, so an effect that times out may be attempted again. For a refund or a payment, the agent cannot tell whether the first attempt reached the target. A retry the target cannot recognise can run the effect twice.

An effect of class irreversible with two or more attempts must now declare a guarantee: idempotent header "<Name>" window <duration>, a key the runtime attaches to every write request in a capability the handler cannot bypass, or idempotent by nature, for the standard library's own effects on a pinned list. Otherwise the check reports PL4003 UNGUARDED_RETRY with a witness, and admission refuses the build unless a person has signed an acceptance.

effect refund(amount: 0..500, customer: Principal, order: Items) {
  kind "payments.refund"
  class irreversible
  retry { attempts 3, base 200ms, timeout 30s }
  idempotent header "Idempotency-Key" window 24h
  ok -> Refunded()
  failed -> Declined()
}

An illustrative refund effect. Remove the idempotent line and the check answers PL4003.

PL4003 UNGUARDED_RETRY  refund
  delivery: Propose, GateAllow, Start (target may execute), HandlerFailed,
            Start (target may execute), HandlerOk, SettleOk
  executions of the target: 2, idempotency key: unchanged, deduplication declared: none
verdict: FINDINGS (exit 1)

The window must cover the retry horizon (PL4004 KEY_WINDOW_TOO_SHORT), and an effect that reaches outside must declare its class (PL6304). The finding says that a delivery exists in which the target may run twice; it does not say that a provider duplicates. Two assumptions are named in the certificate whenever an effect relies on them, and poly verifies neither: a target honours the key it is sent (K17), and an effect declared idempotent by nature is (K18).

What retry safety covers, and what it does not

The key is the intent's id: a digest of the instance, the step's sequence number, the effect's kind and its ordinal. It is not derived from the order or the payload. So the guarantee is effectively once, per intent, under K17. It covers the runtime retrying one request. It does not cover the program forming a new intent for the same refund, for example when a customer asks again after an uncertain outcome. That intent carries a new key, and the target sees a new request.

A path property covers it, if the author writes one and the program keeps the state it needs. In the demo's poly build, each order is its own machine, and an uncertain refund moves to Review, which only an operator leaves. A property over a ghost field states the rule. Its core clause is below; with the field and its three updates, it is eight lines:

never no-reissue-i: emit refund(li: true) while issued[i]

On the build as written the check is CLEAN. Change the uncertain outcome to return to Idle and the check answers PL3002 with a six-step witness: open, request, confirm, outcome unknown, request, confirm. In v1.3.0 the concierge example had no such state and no such property: an uncertain refund was delivered as a failure, the desk returned to idle, and a second request emitted a second refund. v1.3.1 adds a refund ledger to its desk (None, Unknown, Issued), an uncertain outcome that only a person's signed decision settles, and the property no-reissue. Live, two requests for 40 now give one refund and the reply "already processed". The ledger is per conversation, not per order: a cited order has no readable identity in the program yet.

A target that offers no key (an email, a message) declares one attempt. That is at most once, and an ambiguous end is delivered to the program as a completion. Routing it to a person, as the inbox does, is a convention of the program; the spec does not check it.

The rule is shown end to end in the refund demo: two agents build the same refund agent from one prompt; both choose a key; with the key removed, the TypeScript build passes most of its own tests and refunds a customer twice, while the poly build is not admitted.

Where it stands

What we measured

Before building the runtime, a first experiment had coding agents implement the same stateful features in four arms: TypeScript alone, TypeScript with polygraph after the fact, poly, and poly embedded in TypeScript. Over 200 runs, every poly run produced an admitted program, although poly is not in any model's training data. That shows agents can write admitted poly on tasks of this size. Whether they do on hard tasks is not measured yet. The tasks were too easy to separate the arms: the TypeScript arms had no escaped defects, so a reduction had no room to show. Most poly defects came from one trap, domains that accepted values outside what was checked. Version 1 made strict domains the default, and a follow-up run measured it: 0 of 20 runs with an escaped defect, against 5 of 20 before the change (one-sided Fisher p = 0.024).

The checked agent harness

The harness is the loop around a coding agent, written in poly: the turn, the context window and the trial are machines. It holds the four mechanisms of SoL-Pi (NVIDIA and MIT): Action Fusion, Online Context Compact, ObservationPack and the Evidence-Preserving Reducer. The rules that make each one safe to switch on are invariants the checker checks, with a seeded fault for each. A live run then ran 40 trials on 12 small tasks, with Claude Opus 5.5 as the agent, every command in a disposable container with no network.

• Every trial finished every stage, with and without the mechanisms, so completion could not tell them apart. The verdict is INCONCLUSIVE, as predicted in writing before the run.
• The mechanisms fired where they had something to act on. Fusion took 36 of 38 opportunities, ObservationPack archived all 9 large outputs, and the Reducer's 7 summaries were all verified. Compaction never fired: no context grew past half its window.
• Poly's own accounting matched the provider's usage on every call. The run cannot show a saving from the mechanisms. That needs long tasks, which are a candidate for a later release.

The refund demo

The v1.3 demo measured the rule on agent-written code. Two coding agents got the same prompt, a WhatsApp refund agent that talks to Stripe, one in TypeScript and one in poly. Replayed offline with the first answer lost, both kept builds refunded once: each had chosen an idempotency key unprompted. With the key removed, the TypeScript build still passed 18 of its 20 tests and, on a one-item request, refunded the customer twice (80.00 for 40.00 asked); the poly build was PL4003 and was not admitted. In a live rehearsal over Claude Haiku 5.5 and Claude Opus 5.5, the checked concierge refused 5,000 at dispatch, held a 450 refund for a person's approval and then refused it against the 120.00 charge, and showed no guest another's order. Both builds also refunded the wrong amount, which poly does not check. The details and the runbook are on the refund demo’s records in the repository.

What poly is not

• Not a general-purpose language. Computation that is not state-machine logic stays in the host language, TypeScript first.
• Not a proof system for unbounded domains. Checks are exhaustive over declared finite domains, and those domains are printed with every verdict.
• Not a harness. A harness governs what an agent may do while it works. Poly governs what the program may do after the agent is gone.

What poly does not cover

Every limit below is stated in the certificate of the program it applies to. A reader can check what poly promises against this list.

• Composition has a size limit. Machines that exchange messages are checked jointly, over global states, with a bound on the messages in transit; a search that hits the bound is INCONCLUSIVE. The cost grows fast. In one measured case it went from 52 global states for one copy of a machine to 898 for two and 17,992 for three, and four copies did not finish. In the harness, its three main machines are checked one at a time: checking them in pairs was inconclusive with up to two messages in transit, and ran out of memory with three. Their joint behaviour is an open assumption. The projection rule of v1.2 helps only where its three conditions hold.
• Handlers are host code. The machines are checked. The TypeScript that carries out an effect is held by capabilities, a lint and tests, not by the checker. In the refund demo, both builds refunded the wrong amount: the amount was computed in a handler, outside the machine.
• Retry safety rests on the target, and is per intent. A declared key is attached on every attempt of one intent, but that the provider honours it (K17) is an assumption, stated in the certificate and not verified. A second intent for the same refund carries a new key; only a path property the author writes rules it out.
• The lowering is validated per program, not proved. poly-ref compares every transition of the checked instance with the lowered module (226,950 transitions for the concierge's desk). No mechanized proof covers the compiler.
• Finite answers declassify. An enum answer to a question about private data carries no taint (section 3).
• People can be wrong. In the inbox, an owner who answers "missing" when a draft exists can get a second draft.
• Isolation is the container's. The harness ran every model-written command in a container. An escape from the container runtime is outside what poly checks.
• Domains are declared. Checks are exhaustive over the declared finite domains and the opaque representatives, and the verdict prints both. A property that needs a larger domain needs a larger check.

Conclusion

Poly gives frontier models a small, readable language whose checker explores every reachable state and answers with witnesses and typed fixes. It gives AI applications a runtime where every effect crosses a gate, every model answer is a typed value already explored, and every run replays from its journal. With v1.1, those journals return to the checker: rules learned from real runs are adjudicated by a person and checked before they become part of the program. The inbox shows the whole cycle on one defect, from a mined rule to a witness, a fix and a checked invariant. With v1.3, that class of defect is found from the declaration alone: an irreversible effect that may be retried must say how the target keeps it to once per intent, and a path property can rule out a second intent for the same refund. The refund demo shows the difference that makes on code two agents wrote from the same prompt. What poly does not cover is listed beside what it does, so a verdict can be read for exactly what it covers.

Glossary

Action

A named input a machine accepts, with typed parameters.

Admission

The step that refuses an unchecked build and writes the certificate for a checked one.

Certificate

The signed record binding a source to its lowered artefacts, check results and assumptions.

Check domain

The finite set of values a field or parameter is checked over.

Deadlock

A reachable state that is not terminal and in which no action is accepted.

Decision

A model call whose answer is a finite typed value.

Effect

A declared action on the outside world, emitted by an accepted step.

Fairness

The stated assumption that a listed action group, if it stays enabled, is eventually taken.

Gate

The runtime component that allows, denies or escalates each effect.

Handler

The host code that carries out an effect, with only the capabilities its labels grant.

Idempotency key

A header that lets the target recognise a repeated request and return its first answer instead of acting twice.

Invariant

A property that must hold in every reachable state.

Journal

The hash-chained, signed record of every step and gate decision.

Liveness property

A property that something eventually happens, checked under its stated fairness.

Lowering

Turning one poly source into the artefacts each engine reads.

Machine

A declared state machine: state, actions, handlers, effects and properties.

Opaque type

A type a program may only store, pass and compare for equality (Content, Key, Principal, Items), checked by representatives.

Path property

A property over the sequence of effects a machine may emit.

PL4003

The finding for an irreversible effect that may be retried with no declared guarantee that the target runs it once.

Policy

A file of obligations that decide when effects are allowed.

Promotion

Turning an adjudicated rule into checked source, with the rule it came from cited.

Refinement check

The check that the lowered module and the machine agree on every reachable state and input of the instance.

Replay

Rebuilding every state and decision from the journal alone, with no outside call.

Retry safety

The v1.3 rule that an irreversible effect with two or more attempts declares a key or is idempotent by nature. The guarantee is effectively once per intent, under K17.

Ghost field

A state field kept only so that a property can refer to it, such as "a refund for this line was issued".

Taint

The audience class and owners a body or item set carries, followed by the check through effects and messages, and by the gate into model calls.

Terminal state

A state a machine declares as an end; stopping there is not a deadlock.

Verdict

The single result of a check: CLEAN, FINDINGS, REFUSED, UNDERPOWERED or INCONCLUSIVE.

Witness

A concrete, replayable sequence of steps that shows a finding.