In a factory where agents write most of the code, the review queue stops being a bottleneck and starts being a fiction — nobody reads it all. The replacement is not more tests. It is a different relationship between a claim and its evidence: laws checked over thousands of random cases, verdicts that carry their reasons, published commands that would prove the page wrong, and three defects that print FALSIFIED in red on purpose.
01 · Definition
CI answers "did the code I wrote still do what my examples said?" Continuous verification answers "does the property I claimed still hold across the space of inputs, and can a reader check that independently?" The difference is the quantifier. An example test asserts something about the cases you thought of. A property test asserts something about all cases and then hunts for a counterexample. Only the second survives being written by a machine that is also writing the code.
| Layer | The question it answers | Fails when | Survives agent-written code? |
|---|---|---|---|
| Example test | Does f(2) return 4? | A case you enumerated breaks | No. The agent that wrote the code can write the examples that pass. |
| Type check | Do the shapes line up? | A shape mismatch | Partly. Types cannot express "and it computes the right thing". |
| Property test | Does f(a∘b) = f(a)∘f(b) for randomly generated a, b? | A counterexample is found in N trials | Yes — the law is stated independently of the implementation. |
| Certificate | Why did this specific decision come out this way? | The reasons don't reconstruct the verdict | Yes, and it is the only layer that is auditable after the fact. |
| Falsification table | What would prove this page wrong, and what command shows it? | A reader runs the command and sees the killing observation | Yes. It moves the burden from trust to reproduction. |
02 · The shape of a law
The eight-rung governance kernel is deliberately built out of small algebras — monoids, lattices, semirings — because algebras come with laws, and laws are mechanically checkable in a way that prose requirements are not. Each one translates back into something an operator would actually want to know.
| Law | Formally | The engineering question it is |
|---|---|---|
| Associativity | (a ∘ b) ∘ c = a ∘ (b ∘ c) | Does it matter how I bracket a pipeline? If not, the scheduler is free to regroup work. |
| Identity | a ∘ id = a | Can I insert a no-op stage without changing the result? If not, refactoring is unsafe. |
| Annihilation | u ⊗ 0̲ = 0̲ | Can a high score resurrect a forbidden option? This is the safety floor, stated arithmetically. |
| Commutativity | a & b = b & a | Does the order I combine two capabilities change the verdict? It should not — and in one case it does. |
| Monotonicity | a ≤ b ⟹ f(a) ≤ f(b) | Can adding evidence ever lower confidence? If yes, the system punishes investigation. |
| Entrenchment | amend(core) = ⊥ | Can the system rewrite its own safety floor? The one law an autonomous factory cannot do without. |
Pass the laws in your language; you are conformant. — which is why the laws are the specification rather than a test of it. Two conformant hosts in two languages are not "compatible"; they are provably identical, the way two calculators agree on 2 + 2.
03 · Trials
If a law is violated on a fraction p of the input space, the chance that N independent random trials all miss it is (1 − p)^N. That is the entire statistical content of a property suite, and it is worth being precise about because it cuts both ways: a passing suite is evidence of rarity, never of absence. Move the slider and watch how fast the guarantee decays for rare defects.
04 · The artifact
The object a governed decision returns instead of a boolean. It names what was forbidden, what was infeasible, what it cost, what was known, and why the surviving option survived. The test of a certificate is simple: can a third party reconstruct the verdict from it without re-running the system? If not, it is a log line wearing a formal name.
The homepage's bridge demo runs this live: toggle permitted off
and drag utility to the ceiling. The forbidden option stays 0̲ and the certificate says
deontic veto rather than score too low. Those are different facts and a boolean cannot
tell them apart.
This is the same discipline as the ? marks on the factory floor: a
missing rung renders ?, never a flattering spec, because
an invented status is worse than a missing one — it stops the question being asked.
Absence of evidence has to stay distinguishable from evidence of absence, in the data structure, not just
in the prose.
05 · The part most sites delete
CP5, CP6 and CP7 are declared-open gaps in the composition algebra,
rooted in the Value.pi carrier. They are not hidden, skipped, or marked pending.
They run every build, print FALSIFIED in red, and are expected to.
| Gap | The law it breaks | Why it is open rather than fixed |
|---|---|---|
| CP5 | The |> floor is association-invariant: isZero((a|>b)|>c) === isZero(a|>(b|>c)) | A real soundness bug in re-association, not a test artefact. |
| CP6 | No backward execution step survives |>, in either association | Same root cause as CP5 — symptom 1 of the carrier defect. |
| CP7 | &-operand order does not change a downstream |> floor | Symptom 2. The merge sets its phase by first-non-null, so (A&B) and (B&A) exit at different phases. Reproducible in your browser — press swap. |
process.exit((total === 0 && xpass === 0) ? 0 : 1) — the build fails if an enforced law
fails or if a known gap starts passing. A gap that begins to pass means the carrier fix landed and
it must be promoted into a real suite; leaving it in the xfail list would silently convert a fixed defect
into a permanent excuse. The only thing worse than a red law is a red law nobody notices turned green.
06 · Scope
| Limit | Status | Consequence |
|---|---|---|
| Semantic correctness | out of scope | A type-correct, law-abiding, fully certified composition can compute entirely the wrong thing. No gate described here detects it. |
| Rare defects | bounded | §03's arithmetic: 2000 trials is weak evidence against one-in-a-million violations. Green is not proof. |
| The specification itself | out of scope | Laws verify the implementation against the spec. Nothing verifies that the spec was the right one to write. |
| Verification of the factory end to end | not measured | There is no benchmark of the whole line running. The factory simulator is arithmetic, not telemetry, and says so. |
| The world and authority joins | specified, not wired | Two fields the algebra carries and composition never gates on. Verified code, unverified join. |
The honest summary: this machinery makes a specific class of defect impossible and leaves a larger class untouched. That is still worth building, because the class it closes — silent violation of a stated invariant — is exactly the class that a human review queue stops catching once the volume of machine-written code passes what anyone reads.
07 · The ending this page has to have
Commands carry their directory. Run them from the repository root and they fail with
MODULE_NOT_FOUND, which on a page about verification would be an unusually embarrassing defect.
| Claim | Status | Command | Expected | What kills it |
|---|---|---|---|---|
| 210 enforced laws, derived not typed | running | cd AmpersandBoxDesign/box-and-box && node test/laws.mjs && node test/compose-laws.mjs |
109 kernel + 101 compose, both totals printed by the suites themselves | A total on this page that no suite prints. The published and printed counts drifted apart once before, which is why nothing here is hand-typed. |
| Every law runs 2000 trials | running | cd AmpersandBoxDesign/box-and-box && grep -n "const N = " test/laws.mjs |
const N = 2000; |
A smaller N, or a per-law override that reduces it for a law this page cites. |
| The build fails if an open gap starts passing | running | cd AmpersandBoxDesign/box-and-box && grep -n "xpass" test/compose-laws.mjs |
process.exit((total === 0 && xpass === 0) ? 0 : 1) |
Any exit path that returns 0 with xpass > 0. That would make the xfail list a place defects go to be forgotten. |
| CP5/CP6/CP7 currently print FALSIFIED | declared open | cd AmpersandBoxDesign/box-and-box && node test/compose-laws.mjs |
Three ✗ … FALSIFIED @trial N (known gap) lines, and exit 0 |
Fewer than three, without a corresponding promotion into a suite. Or this page describing them as fixed. |
| 2000 trials is weak evidence against rare defects | running | §03 — set p to 1 in 1,000,000 | ≈ 99.8% chance all 2000 trials miss it | The computed value diverging from (1 − p)^N, which you can evaluate yourself. |
| A semantically wrong result passes every gate here | out of scope | Write a function that type-checks, certifies, and returns the wrong answer | It composes cleanly. Nothing on this page objects. | Nothing — this row is the concession, stated before you can catch us with it. |