Agentic SDLC · verification pyramid
A human does not read every line.
A payment system built by an AI agent from a frozen spec. Nobody reviews every line before it ships; four automatic checks stand in for that review, each catching a class of mistake the other three would miss. The whole trick is one boundary: an agent proposes the checks, a deterministic engine disposes by deciding pass or fail, so the model never grades its own work.
What PayFlow is
Seven states, integer money, no floats.
A payment intent moves through seven states. Every amount is whole minor units, never a fraction. There is no dispute or chargeback flow in the first version.
- moneyInteger minor units. No float touches any money path, ever.
- terminalVOIDED and REFUNDED end the intent. Any later operation is rejected and nothing changes.
- ledgerAppend only. Corrections are new entries, and one component writes them.
How a change gets checked
A failure is written for the agent, not a human.
Every change runs the pyramid before it merges. A failure comes back as the violated rule, the shrunk counterexample, or the exact offending import, so the coding agent can act on it and try again.
- blockLayers 0 and 1 gate every commit and stop a bad merge in seconds.
- nightlyLayers 2 and 3 run slower, warn only, and feed drift back into the loop.
- humanPulled in only when a verdict cannot be trusted (needs_human), or a rule does not exist yet and needs a new ADR.
Proof you can run
Change the spec, and the gate stops you.
The safety argument is one claim: you cannot change the frozen spec without the pipeline noticing. So we tested it. We added one new invariant to specs/invariants.md and changed nothing else.
- addedINV-8: the sum of a merchant's captured amounts never exceeds its lifetime authorized total.
- caughtThe blocking suite went red at once. A human moved the contract, and the gate refused the build until the new rule is accounted for: listed in the coverage inventory and given a real oracle in the discovered suite.
- revertedINV-8 was a demonstration, not a real rule. The point stands: a spec change is a deliberate, visible event, never a silent one.
The same gate guards the other direction. If a fresh discovery run silently drops an oracle it used to carry, "covered stays covered" turns the build red too. A real regeneration recently did exactly that, dropping the non negativity oracle, and in doing so exposed a blind spot in this very gate; it was strengthened to anchor on the oracle's own assertion, so it now catches that case as well. The discipline audits itself by being run.
The four checks
Each layer falsifies a different claim.
In plain terms: an invariant is a fact that must always hold (never capture more than was authorized); a metamorphic relation checks that two routes to one result match (100 at once must equal 50 then 50), catching bugs no single run can see; Hypothesis generates thousands of random operation sequences and shrinks any failure to its smallest form; the mutation kill rate is the share of deliberately injected bugs the suite notices.
Is the code even in the right place?
A static contract enforces the layering api → domain → infrastructure and a single writer to the ledger tables.
Once caught: an admin route wired straight into the ledger, bypassing all domain validation. Reported 2 kept, 1 broken and blocked the merge.
Does it behave the way the spec says?
Agent discovered invariants (INV-1..7) and metamorphic relations (MR-1..6) replay against the implementation across thousands of generated situations, plus a concurrency harness.
Once caught: a race no sequential test can express. Sixteen threads sending one idempotency key produced up to six duplicate captures, while the sequential replay stayed green.
Can you trust the checker's own verdict?
This layer tests the triage agent, not PayFlow. Reword a failure without changing its data, and the verdict should not move.
Once caught: a fee misroute verdict flipped from real_bug to bad_relation on a single reword, while reordering and padding never moved it. The fragility is lexical.
Is the suite actually checking anything?
A mutation pass breaks the payment core in small ways and asks whether any test notices. The kill rate is the ground truth on Layer 1.
Once caught: a refund path the suite never reached. 62 of 181 survivors clustered in service.refund. Closing that loop moved the kill rate from a 65.3% floor to 73.1%.
Results
Injected bugs killed by the agent's own suite, with zero hand written test cases.
Every property was discovered by an agent and every counterexample found by Hypothesis. Two checks block a merge, two run nightly and warn until baselined. The whole build cost roughly forty five cents in model calls, estimated from the committed run reports.
The agent suite matches the full local suite exactly, 73.1% both: a hand written Phase 1 sanity machine, run alongside, adds no kills the agent's own rules, invariants, and relations do not already make. So the headline stands entirely on the agent's work. The live numbers, from real run artifacts, are just below.
Trust report, measured
Every number below comes from a real artifact.
Nothing here is hand typed: gate status is run live, kill rates come from the committed mutation baseline, and the discovery funnel is read from each agent run.
Discovery funnel
No agent runs recorded yet.
Layer 3 mutation ground truth
How many injected bugs the suite actually kills.
Kill rate is killed over covered. Mutants on paths a suite never exercises are shown, not folded in to flatter the number. Scope: payflow/domain, payflow/infrastructure/ledger/core.py. Baseline generated 2026-07-11T22:18:26Z, nightly recomputes.
Semantic exploration · informational
Realistic bugs the suite misses, mapped to the frozen spec.
This is not a gate and is separate from the kill rate above. A cross family LLM adversary injects realistic bugs mutmut's syntactic operators cannot express; each survivor is then confirmed by hand against specs/ (ADR-0007: the spec is the referee). A survivor is a candidate gap for a human, not a proven bug. The number is adversary dependent, so a strong score is never mistaken for the gated one.
run: anthropic:claude-sonnet-5 · killed 1 · survived 8 · of 9 · 2026-07-03 13:25 UTC
Frozen spec coverage (survivors confirmed against specs/)
6 full · 2 weak or unreached · 4 absent of 12 frozen rules: where a human pushes discovery next.
| id | frozen requirement | coverage | note |
|---|---|---|---|
| INV-1 | captured_amount ≤ authorized_amount | full | captured_le_authorized invariant |
| INV-2 | refunded_amount ≤ captured_amount | full | refunded_le_captured invariant |
| INV-3 | merchant, holds, platform_fees never negative | full | closed 2026-07-11: the non-negativity check now asserts merchant, holds and platform_fees are all >= 0 once per example (external_settlement, the funding source, may go negative) |
| INV-4 | global debits == credits (conservation) | full | closed 2026-07-11: a once-per-example conservation oracle asserts the net delta across every account this run touched is zero, measured against a per-instance system-account baseline (safe on a shared server since examples run sequentially) |
| INV-5 | transitions only along the state table; nothing from VOIDED or REFUNDED | partial | illegal-state rejection rules cover most transitions |
| INV-6 | preconditions enforced: illegal op returns 409, changes nothing | full | authorize/capture/refund/void illegal-state rules plus assert_unchanged |
| INV-7 | every AUTHORIZED+ intent has ≥ 1 ledger entry pair | absent | no check that a ledger entry pair exists |
| amount ≥ 1 | amount < 1 returns 422 | absent | zero or negative amount never probed (survivor: allow-zero) |
| capture > fee | capture ≤ fee returns 422 | absent | boundary where amount equals the fee never probed (survivor: fee-equal) |
| capture ≤ remaining | capture over remaining hold returns 422 | full | capture_over_limit_rejected |
| refund ≤ refundable | refund over refundable returns 422 | reachability | refund_over_limit_rejected exists; sequence unreached even at 6x budget (survivor: refund-cap-total) |
| idempotency | same key, different endpoint returns 409 | absent | the replay relation replays one endpoint only; no discovered relation crosses endpoints under a shared key (survivor: idempotency-cross-endpoint) |
The pipeline
Who proposes, what checks it, and whether it is green now.
The whole trust argument is one boundary: the LLM proposes (fallible), a deterministic engine disposes by compiling, executing, and scoring. The graph is coloured by that split (from agent/roles.py, drift gated); the gates below are the deterministic side, run live.
Live gate status · all fast gates green
Layer 0 structural and drift plus the Layer 1 replay slice, run live when this page was generated. These are what block a merge.
| layer | gate | result | detail | elapsed |
|---|---|---|---|---|
| Layer 0 | import contracts | PASS | 3 kept, 0 broken | 0.12s |
| Drift | state machine diagram | PASS | 1 passed | 0.58s |
| Drift | importlinter snapshot | PASS | 1 passed | 0.49s |
| Drift | agent graph diagram | PASS | 1 passed | 0.99s |
| Layer 1 | property sanity machine | PASS | 1 passed | 3.12s |
| Layer 1 | idempotent replay (concurrency A) | PASS | 1 passed | 2.19s |