Skip to content

v0.4.0 — Verification

Choose a tag to compare

@arpanghoshal arpanghoshal released this 04 Sep 17:03
· 513 commits to main since this release
2763010

Does it hold in your setup?

pip install ctrlrun
ctrlrun verify

Everything CTRLRun guarantees was proven, until now, by this repository's tests against this repository's configurations. That is the right place to start and the wrong place to stop: what you deploy is your policy, your grants and your store, and a guarantee that has never been exercised against those is a guarantee nobody has checked.

ctrlrun verify runs the kernel's own failure scenarios against the configuration in front of it — in a scratch store, with fake executors, reaching no network — and reports what passed, what failed, and what could not be tested at all.

G1   mutated approval refused         PASS  stripe.refund
G2   replayed approval refused        PASS  stripe.refund
G3   duplicate effect refused         PASS  stripe.refund
G4   one winner under concurrency     PASS  stripe.refund (8 processes)
G5   ambiguous blocks a blind retry   PASS  stripe.refund
G6   unknown action refused           PASS
G7   no principal refused             PASS  stripe.refund
G8   expired authority refused        PASS  head-of-support
G9   delegation cannot escalate       PASS  head-of-support (6 of 6 dimensions)
G10  unknown exception is ambiguous   PASS  stripe.refund

10/10 declared guarantees pass. 0 not applicable.

Not applicable is not a pass. A policy with no approve rule cannot exercise the approval-binding guarantees, so they are reported N/A with the reason, excluded from the denominator and listed separately — 5/5 (5 not applicable), never 10/10. There is no flag that folds one into the count.

Verify never touches your store. .ctrlrun/state.db is byte-identical before and after, and is never created where it did not exist.

Every guarantee carries a positive control. A refusal asserted against a scenario in which nothing ran passes on a kernel with the guard deleted, so each scenario establishes the observable would have been visible had the guard not fired. A control that misbehaves is fail with reason: "control failed" — never a pass, never an N/A.

The badge means "declared guarantees pass" — that phrase, and no other. Not secure, not safe, not compliant, not certified, not audited. docs/verify.md says on the same screen what verify cannot see: your executors, your reconcile hooks, where you put the decorator, your deployment, and whether your policy is the right policy.

pip install ctrlrun still installs nothing but pyyaml and clickincluding all of verify, because a verification tool behind an extra is one half the deployments never run.

Note on versions: 0.3.0 was never published; 0.3.0rc1 was its last tag. This release goes from 0.2.0 to 0.4.0 on PyPI.


Does it hold in your setup? Everything CTRLRun guarantees was proven, until now, by this
repository's tests against this repository's configurations. That is the right place to start
and the wrong place to stop: what an operator deploys is their policy, their grants and
their store, and a guarantee that has never been exercised against those is a guarantee
nobody has checked.

ctrlrun verify runs the failure scenarios of v0.1 §7, v0.2 §10 and v0.3 §10 against the
configuration in front of it and reports what passed, what failed, and — the part that makes
the number mean anything — what could not be tested at all.

Three rules govern it, and each has a test that would go red if it stopped holding. Not
applicable is not a pass.
Verify never touches the operator's store. The badge means
"declared guarantees pass"
, and nothing else. A fourth keeps verify honest about itself:
every guarantee carries a positive control, because a refusal asserted against a scenario
in which nothing ran passes on a kernel with the guard deleted.

No schema changes: ctrlrun.policy/v3, ctrlrun.receipt/v2, ctrlrun.action/v1 and
ctrlrun.inspection/v2 are untouched, and no store gains a table or a column — verify
writes only to a scratch store it created. Three new schema strings belong to documents rather
than to storage: ctrlrun.verify/v1, ctrlrun.guarantees/v1 and ctrlrun.framework-probe/v1.

Added

  • ctrlrun verify — the guarantee catalogue, the scenario engine and all ten guarantees
    (SPEC-v0.4 §2, §3). ctrlrun.verify is core: stdlib, pyyaml and click, because a
    verification tool that needed an extra installed is one half the deployments never run. It is
    not re-exported from ctrlrun and import ctrlrun does not import it.

    It reads the operator's policy document, and the authority document beside it where
    --authority names one, derives concrete actions, principals and delegations the
    configuration actually admits, and runs the failure scenarios of v0.1 §7, v0.2 §10 and
    v0.3 §10 against them — in a scratch store, with in-process fake executors, reaching no
    network. G1 mutated approval refused · G2 replayed approval refused · G3 duplicate
    effect refused · G4 one winner under concurrency, across real OS processes · G5 ambiguous
    blocks a blind retry · G6 unknown action refused · G7 no principal refused · G8 expired
    authority refused · G9 delegation cannot escalate, on every dimension the parent constrains
    including the omission case · G10 unknown exception is ambiguous, never failed.

    Every guarantee carries a positive control. A refusal is satisfied just as well by a
    scenario in which nothing ever ran, and that scenario passes against a kernel with the guard
    deleted — so each scenario runs a companion establishing that the observable would have been
    visible had the guard not fired. A control that does not behave as specified makes the
    guarantee fail with reason: "control failed": never a pass, and never an N/A.

    There is no randomness anywhere — not seeded randomness, none. Selection is sorted by
    codepoint, values come from a fixed table, the candidate search is bounded at 64, and two runs
    against one document produce byte-identical JSON once the timestamps are removed.

  • ctrlrun verify [--authority PATH] [--json] [--junit PATH] [--only G1,G3] [--store-url URL],
    replacing the v0.3 stub. Exit codes: 0 every applicable guarantee passed and at least one was
    applicable, 1 a guarantee failed, 2 the configuration was refused or is unusable, 3 an
    internal error in verify itself.

  • Reporting (SPEC-v0.4 §4). The human report is one line per guarantee in catalogue order,
    every N/A carrying the reason that made it one, with the summary as the last line so a
    tail -1 is meaningful. --json emits one ctrlrun.verify/v1 document carrying the SHA-256
    of both documents verify read — a report and a policy that do not hash the same are a report
    about something else — and a counterexample only on a fail, because a counterexample
    on a pass would be evidence of a failure that did not happen. --junit PATH writes a JUnit
    XML file in which an N/A is <skipped> and never a pass, which is the same rule as
    everywhere else expressed in the vocabulary a CI dashboard already has.

    JUnit XML has no normative schema, and the report says so rather than implying one: T115
    validates against tests/data/junit-10.xsd, a checked-in copy of the de-facto Windy Road
    schema with its provenance and Apache-2.0 licence recorded beside it, and asserts the
    document structurally as well — a permissive schema is not a check. xmlschema joins the
    dev extra for that test and for nothing else.

  • The GitHub Action, the badge and docs/verify.md (SPEC-v0.4 §5). action.yml at the
    repository root is a composite action: it installs ctrlrun, runs
    ctrlrun verify --json --junit, renders the job summary and the badge from that report
    rather than from a second run — so the badge, the summary and the uploaded artifact can never
    disagree about what happened — and uploads the three files as one artifact.

    It fails the job when a guarantee failed and when the configuration was refused, and succeeds
    when guarantees are N/A. There is no input that makes a failure not fail the job: a
    continue-on-error-shaped flag here would be a flag that makes a consequential thing
    permissive by default, and a workflow that wants to tolerate a failure has
    continue-on-error on the step already, where it is visible.

    The badge is a Shields endpoint JSON the action writes and never publishes. Committing it
    would need contents: write in every consumer's workflow, and asking for write access to a
    repository as the price of a verification badge is a bad trade for a tool whose subject is
    least privilege; docs/verify.md shows the one-job publishing pattern once, with its cost
    visible. Rendered, it reads exactly CTRLRun verified N/M, where M is applicable
    guarantees and never the catalogue size. A partial run and a run that exited 2 or 3 write no
    badge at all.

    The badge means "declared guarantees pass" — that phrase, on the badge's link target, and
    no other. Not secure, not safe, not compliant, not certified, not audited.
    docs/verify.md#what-the-badge-means says it in its first sentence and, on the same screen,
    what verify cannot see: the operator's executors, their reconcile hooks, where they put the
    decorator, their deployment, and whether the policy is the right policy.

    This repository's CI runs the action against examples/authority/payments.yaml (10/10) and
    against examples/policies/payments.yaml (5/5, 5 not applicable), asserting both shapes
    so a change that made verify silently count N/As as passes is caught in CI rather than in a
    badge.

  • docs/OWASP-AGENTIC-TOP10.md (SPEC-v0.4 §6) — a reading of the OWASP Top 10 for Agentic
    Applications (2026 edition, announced 2025-12-09) against the ten guarantees. Its first line,
    before any table, says what it is not: not a compliance claim, not a conformance claim, not a
    certification, and not a statement that CTRLRun covers the Top 10.

    Two tables, and the second is what makes the first credible. ASI04 supply chain, ASI05
    code execution and ASI06 memory and context poisoning are not CTRLRun's subject
    nothing here inspects a package, sandboxes an interpreter or reads a model's memory — and
    ASI07 inter-agent communication waits on v0.7. ASI01 agent goal hijack and ASI09
    human-agent trust exploitation appear in both tables, because CTRLRun constrains what a
    hijacked agent can do without detecting the hijack, and binds an approval to one action
    without authenticating the approver or noticing that they were misled.

    The document records how its codes and titles were derived, because the published PDF sits
    behind a download form and could not be retrieved: they come from the OWASP-owned
    OWASP/secure-agent-playbook repository, corroborated against two independent summaries, and
    the four places where a third summary disagreed are named. That correction is what SPEC-v0.4
    §6.2 marked its own provisional list as needing.

  • research/framework-probe/ (SPEC-v0.4 §7) — a research harness that drives the
    double-refund and approval-mutation scenarios through third-party agent frameworks against a
    fake remote, and emits a table. It lives outside src/, is never imported by ctrlrun, and
    its per-framework dependencies are never installed by ctrlrun or by any of its extras.

    Its README's first paragraph says what the table is: behaviour, not quality. A framework
    that retries a lost response is doing what its documentation says it does; the finding is
    about what an agent stack does without an effect-level guard.

    One fake remote for every framework, with three behaviours — commit-then-drop,
    commit-then-timeout, capture-what-was-approved — counting effects by identity, not by
    request
    , so "executed twice" means two effects and not two HTTP calls. Every outcome is
    derived from what the remote saw and never from anything an adapter reports about itself.

    Two stub frameworks run by default and disagree: one retries and reports executed_twice,
    one does not and reports executed_once. Without the pair, a harness hard-coded to say
    executed_twice would pass its own tests and say the same thing about every real framework
    it ever ran.

    No results are checked in, and a test asserts it. The runs are made and published by the
    maintainer; a commit carrying findings about other projects that nobody had reviewed is not
    one this repository makes.

  • The badge this repository shows is published, by a badge job scoped as narrowly as the
    thing it does: contents: write at job level (the workflow is contents: read, so
    nothing else in it can write), running on a push to main and on nothing else — a pull
    request from a fork must not be able to write the badge, and a read-only fork token is a
    default rather than a refusal — and publishing the badge the verify job already produced,
    downloaded as an artifact rather than regenerated, so §5.1's one-run rule holds across the
    job boundary. docs/verify.md shows the job and names the permission it costs.

  • docs/SPEC-v0.4.md gains a §12, recording the readings the implementation had to take
    where the specification could not be satisfied as written. A specification that
    disagrees with the code it describes is worse than one that admits a gap: G6 drives a
    a guarantee's invariant is the behaviour and not one reason string — G6 asserts that an
    unlisted action never executes, against the Control the operator's configuration actually
    composes, accepting any reason that configuration can produce and reporting which one fired,
    because under an authority: section the refusal correctly arrives from the authority axis
    before policy is reached; G7 is N/A
    where no action in the policy can run, because §2.2 said "never" and §1.3 requires a control
    that such a policy cannot supply; G8 gains a fourth N/A reason for a layered document; G9's
    control names the delegation only where the parent's subject does not also match it; and
    G4's children are subprocesses rather than multiprocessing, which would re-import the
    caller's __main__ in every child.

Changed

  • docs/SPEC-v0.3.md §10 T85 is amended, as SPEC-v0.4 §9.4 item 2 requires and in the
    commit that made it true: ctrlrun verify exits 2 under mode: observe with a message naming
    the mode, and runs under mode: enforce. The banner assertions for every other command are
    untouched. A frozen test whose subject was explicitly temporary is amended rather than
    deleted.

  • docs/SPEC-v0.3.md §4.3.1 gains an informational row for ctrlrun.verify.run (SPEC-v0.4
    §3.9, §9.4 item 3). Verify is not a new entry point: it proposes no action of its own and
    drives the rows already there. The row exists because a reader will look for one.

  • docs/ARCHITECTURE.md §6's module map gains verify/, above control.py and beside cli/.

  • docs/SPEC-v0.4.md — the v0.4 contract, a delta over v0.1, v0.2 and v0.3. v0.4 answers
    the question the first three releases could not: does it hold in my setup? Everything
    CTRLRun guarantees is proven today by this repository's tests against this repository's
    configurations, which is the right place to start and the wrong place to stop.
    ctrlrun verify runs those failure scenarios against the operator's own policy, grants and
    store type, and reports what passed, what failed, and what could not be tested at all.

    Three rules govern it. Not applicable is not a pass: a configuration with no approve
    rule cannot exercise the approval-binding guarantees, so they are reported N/A with the
    reason, excluded from the denominator, and listed separately — 3/3 (5 not applicable),
    never 8/8. Verify never touches the operator's store: every scenario runs against a
    scratch store created and destroyed with the run, and .ctrlrun/state.db is byte-identical
    before and after. The badge means "declared guarantees pass" — that phrase, on the
    badge's link target, and never "secure" or "compliant".

    Nothing is implemented yet. The specification is the contract the seven build-list items are
    written against.