Conformance · the laws are the spec

97 laws.
Every one a property test.

The verdict is the contract. box-and-box isn’t defined by an implementation — it’s defined by these laws: associativity, the annihilation of a veto, the precedence of the bridge, the un-weakenability of the entrenched core. Each is checked against 2000 random cases on every run. Two hosts, in any language, must agree on all 97. Pass them, and you’re conformant — the way an implementation is POSIX because it passes the suite, not because it says so. Click any law to see its formal property and what it guarantees.

8
modal subsystems
97
property-tested laws
2000
trials per law
1
verdict, certified
  reproduce it yourself live output 
$ npm i -g box-and-box && node test/laws.mjs

box-and-box law harness · 2000 trials/law
──────────────────────────────
Feasibility (L1–L14): 14/14 pass
Priority    (H1–H13): 13/13 pass
The bridge  (B1–B3):  3/3 pass
Permissions (D1–D9):  9/9 pass   · composition (DB1–DB3): 3/3
Time        (T1–T8):  8/8 pass   · composition (TB1–TB3): 3/3
Economy     (C1–C8):  8/8 pass   · composition (CB1–CB3): 3/3
Knowledge   (E1–E8):  8/8 pass   · composition (EB1–EB3): 3/3
Coordination(S1–S8):  8/8 pass   · composition (SB1–SB3): 3/3
Self-amend  (R1–R8):  8/8 pass   · composition (RB1–RB3): 3/3
──────────────────────────────
✓ all 97 stated laws hold.
The bridge
composition · 3 laws

feasible ▸ permitted ▸ best — the rule that composes the rest, and the annihilation that makes a veto absolute.

B1▸veto ⇒ score 0̲✓
propertyinfeasible(o) ⇒ gatedScore(o) = 0̲ (−∞)
guaranteesAn option that fails the feasibility floor scores the tropical annihilator — no amount of utility can lift it back into contention.
B2▸select ranks within feasible✓
propertyselect = argmax utility over the feasible set only
guaranteesThe chosen option is always feasible, and no feasible option out-scores it. Ranking happens strictly after the floor — never across it.
B3▸conservativity: one feasible ⇒ chosen✓
property|feasible| = 1 ⇒ that option chosen (even vs. utility 999)
guaranteesA lone feasible action wins regardless of how attractive the infeasible alternatives look. Feasibility is not a tiebreaker — it is a gate.
Feasibility
alethic · 14 laws

what can happen, the monoid of values, and the 0̲ that infeasibility collapses to.

L1▸combine associative✓
propertycombine(combine(a,b),c) = combine(a,combine(b,c))
guaranteesMerging values is grouping-independent — you can fold a stream of evidence in any order and reach the same state.
L2▸combine identity V0✓
propertycombine(a, V0) = a
guaranteesThe empty value is a true unit — merging in “nothing” changes nothing.
L3▸commutative families (n,κ,β,σ,deny)✓
propertycombine(a,b) = combine(b,a) on each field
guaranteesMerge order doesn't matter — the basis for conflict-free (CRDT) convergence across replicas.
L4▸β idempotent under min✓
propertycombine(a,a).β = a.β (β merges by min)
guaranteesConfidence merges conservatively (lowest wins) and re-merging a value with itself is stable.
L5▸σ idempotent under ∪✓
propertycombine(a,a).σ = a.σ (σ merges by ∪)
guaranteesThe capability set merges by union, so duplicates collapse and self-merge is a no-op.
L6▸κ idempotent under ∨✓
propertycombine(a,a).κ = a.κ (κ merges by ∨)
guaranteesThe cyclicity flag merges by OR and never flips spuriously on re-merge.
L7▸promote β-monotone✓
propertypromote(a, ev).β ≥ a.β
guaranteesEvidence can only raise confidence, never silently lower it.
L8▸reconcile antitone + idempotent✓
propertyreconcile(a,T).σ ⊆ a.σ, and reconcile is idempotent
guaranteesReconciliation only narrows the capability set and reaches a stable result in a single pass.
L9▸deliberate κ→false + idempotent✓
propertydeliberate(a).κ = false, and deliberate is idempotent
guaranteesDeliberation clears a detected cycle and is a fixpoint — running it again changes nothing.
L10▸chain refuses a backward phase✓
propertyphaseIdx(a) > phaseIdx(b) ⇒ chain(a,b) errors
guaranteesThe pipeline cannot run a phase backward — composition respects phase order.
L11▸chain associative where defined✓
propertychain assoc. on forward-ordered triples
guaranteesWhere the pipeline is legal, its composition is associative — sub-pipelines compose predictably.
L12▸promote distributes over combine on β✓
propertypromote(combine(a,b)).β = combine(promote a, promote b).β
guaranteesPromoting then merging gives the same confidence as merging then promoting — order of evidence vs. merge is irrelevant.
L13▸consume gate (β_min)✓
propertyconsume(a).ok ⟺ a.β ≥ β_min
guaranteesThe feasibility gate fires exactly at the confidence threshold — no margin, no slack.
L14▸deny_default idempotent under ∧✓
propertycombine(a,a).denyDefault = a.denyDefault (merges by ∧)
guaranteesDeny-by-default merges by AND — once any source denies, it stays denied, and self-merge is stable.
Permissions
deontic · 12 laws

obligation, prohibition, conflict, and contrary-to-duty repair — and how a permit composes into the verdict.

D1▸join commutative + associative✓
propertyjoin(a,b) = join(b,a), join associative
guaranteesPermission statuses combine order-free — the deontic lattice is a join-semilattice.
D2▸join identity OPTIONAL + idempotent✓
propertyjoin(a, OPTIONAL) = a, join(a,a) = a
guaranteesOPTIONAL (no constraint) is the unit, and joining a status with itself is a no-op.
D3▸O ⊔ F = CONFLICT✓
propertyjoin(OBLIGATORY, FORBIDDEN) = CONFLICT
guaranteesAn obligation and a prohibition on the same act surface as an explicit CONFLICT — never silently resolved.
D4▸join monotone (a ⊑ a⊔b)✓
propertyrank(a ⊔ b) ≥ rank(a) and ≥ rank(b)
guaranteesJoining never lowers deontic strength — constraints only accumulate upward.
D5▸CONFLICT absorbs✓
propertyjoin(CONFLICT, a) = CONFLICT
guaranteesConflict propagates through further joins until it is explicitly resolved.
D6▸resolve idempotent + clears conflict (distinct prio)✓
propertyresolve with distinct priorities clears CONFLICT; resolve idempotent
guaranteesPriority-based resolution terminates a conflict in one pass and re-running it is stable.
D7▸factual detachment (in force iff condition)✓
propertydetach(duty).inForce ⟺ condition holds
guaranteesA conditional duty is in force exactly when its triggering condition is true — no earlier, no later.
D8▸CTD partiality (repair iff violated)✓
propertyrepair present ⟺ primary duty violated
guaranteesA contrary-to-duty (reparative) obligation fires only on an actual violation — not pre-emptively.
D9▸comply: O⇒¬F (ought is permitted)✓
propertycomply(O,done)=ok; comply(F,done)≠ok; comply(O,¬done)≠ok
guaranteesWhat is obligatory is permitted; doing the forbidden, or omitting the obligatory, both fail compliance.
composition (DB1–DB3)
DB1▸forbidden excluded from decision✓
propertyforbidden option (utility 99) is never chosen; safe option wins
guaranteesPermissions sit above priority — utility 99 cannot beat a prohibition.
DB2▸obligation forces over higher score✓
propertyobligatory(utility 1) chosen over non-obligatory(utility 99)
guaranteesA duty overrides mere desirability — the kernel does the obligatory thing even when something flashier scores higher.
DB3▸alethic precedence ⇒ CTD escalation✓
propertyobligatory option infeasible ⇒ decision null + CTD escalation
guaranteesWhen you can't do your duty, the kernel escalates (contrary-to-duty) rather than faking compliance — feasibility still comes first.
Priority
axiological · 13 laws

how the feasible, permitted options are ranked — in a semiring, so preferences never resurrect a vetoed one.

H1▸⊕ commutative monoid✓
property⊕ commutative, associative, identity 0̲
guaranteesAlternatives combine order-free with a zero element — the “choose between” operator is well-behaved.
H2▸⊗ monoid✓
property⊗ associative, identity 1̲
guaranteesSequencing scores is associative with a unit — the “and then” operator composes cleanly.
H3▸left distributivity✓
propertya ⊗ (b ⊕ c) = (a ⊗ b) ⊕ (a ⊗ c)
guaranteesSequencing distributes over choice — a sound preference algebra, not ad-hoc arithmetic.
H4▸right distributivity✓
property(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)
guaranteesDistributivity holds on both sides — confirming a genuine semiring structure.
H5▸0̲ annihilates ⊗✓
property0̲ ⊗ a = 0̲
guaranteesTHE annihilation law — a vetoed option (0̲) times any utility stays 0̲. This is what makes a veto absolute in the score algebra.
H6▸⊕ idempotence (dioid only)✓
propertya ⊕ a = a under the tropical dioid
guaranteesBest-of-self is self on the tropical dioid. Deliberately fails under probability/log semirings (see “where the laws bend”) — picking the wrong semiring is a category error the suite catches.
H7▸⊗ monotone in order✓
propertya ≤ b ⇒ a ⊗ c ≤ b ⊗ c
guaranteesScaling by a common factor preserves ranking — sequencing never reorders preferences.
H8▸reinforce η-contraction✓
property|reinforce(u,t,e) − t| = (1−e)·|u − t|
guaranteesA learning update is a contraction toward the target — values converge, they don't oscillate.
H9▸rollout γ-contraction✓
property‖Bu − Bv‖ = γ·‖u − v‖
guaranteesThe Bellman backup is a γ-contraction — value iteration provably converges to a unique fixpoint.
H10▸dominate idempotent + Pareto✓
propertydominate idempotent; no Pareto-dominated survivor
guaranteesThe Pareto frontier is stable and clean — re-filtering changes nothing and no dominated option slips through.
H11▸anneal ε→0 idempotent✓
propertyanneal drives ε → 0, and is a fixpoint there
guaranteesExploration decays to zero — the schedule eventually commits to exploitation.
H12▸softmax shift-invariant✓
propertysoftmax(u, T) = softmax(u + c, T)
guaranteesScores are relative — adding a constant to every utility leaves the distribution unchanged.
H13▸T→0 collapses to argmax✓
propertysoftmax(u, 0⁺) → argmax
guaranteesZero temperature is exactly greedy selection — the continuous knob recovers the hard maximum at its limit.
Time
temporal · 11 laws

safety as an invariant over the whole trajectory; liveness as a horizon obligation.

T1▸G,F idempotent (GGφ≡Gφ)✓
propertyGGφ ≡ Gφ, FFφ ≡ Fφ
guaranteesThe LTL always/eventually operators are idempotent — “always always” is just “always.”
T2▸duality (¬Gφ≡F¬φ, ¬Fφ≡G¬φ)✓
property¬Gφ ≡ F¬φ, ¬Fφ ≡ G¬φ
guaranteesAlways and eventually are De Morgan duals — negation pushes cleanly through the temporal modalities.
T3▸∧,∨ commutative + idempotent✓
property∧, ∨ commutative and idempotent
guaranteesThe propositional layer under the temporal operators is a well-formed lattice.
T4▸progression faithful (monitor ≡ direct)✓
propertymonitor verdict = direct trace semantics
guaranteesThe incremental runtime monitor is sound — stepping a formula forward agrees with evaluating it over the whole trace.
T5▸safety finite-witness / liveness never-early✓
propertysafety emits a 'vio' witness at the breach step; liveness never commits false early
guaranteesSafety violations are caught at the exact step they occur; liveness is never failed prematurely (it may still be satisfiable later).
T6▸G/∧ and F/∨ distribute✓
propertyG(a ∧ b) ≡ Ga ∧ Gb, F(a ∨ b) ≡ Fa ∨ Fb
guaranteesThe standard LTL distribution identities hold — invariants and reachability decompose conjunctively/disjunctively.
T7▸until fixpoint (φUψ≡ψ∨(φ∧X(φUψ)))✓
propertyφUψ ≡ ψ ∨ (φ ∧ X(φUψ))
guaranteesUntil satisfies its defining fixpoint equation — the basis for unrolling it into a step-by-step monitor.
T8▸lasso GF/FG + G/F vs unrolling✓
propertyGF = some loop state; FG = every loop state; G/F = unrolled prefix
guaranteesOn lasso-shaped (ultimately periodic) traces, ω-regular monitoring matches the unrolled semantics — “infinitely often” and “eventually always” are decided on the loop.
composition (TB1–TB3)
TB1▸safety shield prunes a violating step✓
propertyresidual rejects a violating next step, accepts a holding one
guaranteesThe watchdog blocks the unsafe next action before it executes — safety is enforced at the step boundary.
TB2▸unmet liveness ⇒ escalation at horizon✓
propertymissed liveness at horizon ⇒ escalate (repair/replan)
guaranteesA deadline that comes and goes unmet triggers an escalate-and-replan, not a silent pass.
TB3▸safety violation ⇒ unsafe verdict✓
propertysupervise returns safe=false at the exact violatedAt index
guaranteesA trajectory breach is reported as unsafe and pinned to the step where it happened.
Economy
resource · 11 laws

a closed, double-entry budget; affine use; and pricing the kernel’s own deliberation.

C1▸conservation under transfer (Σ invariant)✓
propertytotal balance invariant under any transfer
guaranteesThe ledger is closed double-entry — a transfer moves value, it never creates or destroys it.
C2▸no overdraft; balances stay ≥ 0✓
propertyover-transfer ⇒ INFEASIBLE; all balances ≥ 0
guaranteesYou cannot spend what you don't have — the budget never goes negative.
C3▸independent transactions commute (CRDT)✓
propertydisjoint transfers commute
guaranteesNon-overlapping transactions can be applied in any order — the ledger converges like a CRDT.
C4▸linearity — spending depletes (not idempotent)✓
propertyspend twice removes two units
guaranteesConsumable resources are linear — each spend depletes, so re-running an action costs again (deliberately not idempotent).
C5▸reusability — using `!` does not deplete (idempotent)✓
propertyusing a reusable (`!`) skill twice leaves the balance unchanged
guaranteesThe “of-course” modality is copyable — a reusable capability can be invoked freely without drawing down a budget.
C6▸flow monotonicity — depletion only decreases✓
propertyavailable tokens only decrease over a run
guaranteesNo spontaneous refills — a consumable budget moves one direction until explicitly replenished.
C7▸capacity conservation (stability + plasticity)✓
propertytotal capacity invariant under allocate/forget
guaranteesAllocating and releasing capacity conserves the total — no capacity leaks between stability and plasticity.
C8▸no free reclaim — forgetting releases the knowledge✓
propertyforget releases capacity AND the associated knowledge
guaranteesReclaiming capacity isn't free — you give up the knowledge that occupied it. No having-it-both-ways.
composition (CB1–CB3)
CB1▸exhaustion ⇒ infeasible (the alethic 0̲ gate)✓
propertyfeasible ⟺ balance ≥ cost
guaranteesRunning out of resource makes an action infeasible — the economy feeds directly into the alethic floor.
CB2▸cost composes additively along a pipeline (semiring)✓
propertythree staged spends = one lump spend of the sum
guaranteesA pipeline's cost is the sum of its stages' costs — budgeting composes predictably along |>.
CB3▸Type-II repair pricing (value ≥ cost ∧ affordable)✓
propertyrepair invoked ⟺ value ≥ cost ∧ affordable; charges cost
guaranteesThe kernel only pays to repair when the repair is worth its price and the budget can cover it — and it actually deducts the cost.
Knowledge
epistemic · 11 laws

knowledge (S5) vs. belief (KD45); a known-unknown that must route to deliberation.

E1▸factivity T (Kφ → φ)✓
propertyKφ → φ
guaranteesKnowledge is factive (axiom T of S5) — if the kernel knows something, it is true. This is the line between knowing and merely believing.
E2▸distribution K (K(φ→ψ)∧Kφ → Kψ)✓
propertyK(φ→ψ) ∧ Kφ → Kψ
guaranteesKnowledge is closed under known implication — you know the consequences of what you know.
E3▸positive introspection (Kφ → KKφ)✓
propertyKφ → KKφ
guaranteesIf you know something, you know that you know it (axiom 4).
E4▸negative introspection (¬Kφ → K¬Kφ)✓
property¬Kφ → K¬Kφ
guaranteesIf you don't know something, you know that you don't (axiom 5) — the formal basis for routing a known-unknown to deliberation.
E5▸belief consistency D (¬(Bφ ∧ B¬φ))✓
property¬(Bφ ∧ B¬φ)
guaranteesBelief is consistent — the kernel never simultaneously believes a thing and its negation.
E6▸knowledge ⇒ belief (Kφ → Bφ)✓
propertyKφ → Bφ
guaranteesAnything known is also believed — knowledge is the stronger, factive layer above belief.
E7▸learning monotonicity (announce preserves K)✓
propertypublic announcement of a truth preserves prior K
guaranteesLearning a true fact never destroys existing knowledge — the epistemic state only grows.
E8▸common knowledge (Cφ → Eφ)✓
propertyCφ → Eφ
guaranteesCommon knowledge implies everyone-knows — the foundation for coordinated joint action.
composition (EB1–EB3)
EB1▸threshold gate monotone; K = belief@1✓
propertybelief gate monotone in threshold; knowledge = belief at threshold 1
guaranteesRaising the confidence bar can only restrict what counts as believed, and certain knowledge sits at the top of that scale.
EB2▸known-unknown ⇒ deliberate (κ)✓
propertyknowsItDoesntKnow ⇒ route = deliberate
guaranteesA recognized knowledge gap routes the decision into deliberation rather than acting on a guess.
EB3▸pooled knowledge dominates individual✓
propertyindividual knowledge ⊆ distributed knowledge
guaranteesPooling agents' knowledge never loses information — the group knows at least what any member does.
Coordination
strategic · 11 laws

which coalitions can actually ensure an outcome — ought-implies-can, made checkable.

S1▸unit: [C]⊤ and ¬[C]⊥✓
property[C]⊤ holds; [C]⊥ never holds
guaranteesAny coalition can ensure the trivially-true outcome, and none can force the impossible — the floor and ceiling of strategic ability.
S2▸coalition monotonicity (C ⊆ C′ ⇒ [C]φ → [C′]φ)✓
propertyC ⊆ C′ ⇒ [C]φ → [C′]φ
guaranteesA larger coalition can ensure anything a sub-coalition can — adding members never removes power.
S3▸outcome monotonicity (φ⊨ψ ⇒ [C]φ → [C]ψ)✓
propertyφ ⊨ ψ ⇒ [C]φ → [C]ψ
guaranteesIf a coalition can ensure a strong outcome, it can ensure any weaker one it entails.
S4▸superadditivity (disjoint C₁,C₂ cooperate)✓
property[C₁]φ₁ ∧ [C₂]φ₂ ⇒ [C₁∪C₂](φ₁ ∧ φ₂) for disjoint C₁,C₂
guaranteesDisjoint coalitions can pool their guarantees — cooperation achieves the conjunction of what each could ensure alone.
S5▸regularity (¬([C]φ ∧ [N∖C]¬φ))✓
property¬([C]φ ∧ [N∖C]¬φ)
guaranteesA coalition and its complement can't both force contradictory outcomes — the strategic game is consistent.
S6▸maintenance is a greatest fixpoint (□)✓
propertycanMaintain = greatest fixpoint (□)
guaranteesThe set of states from which a coalition can keep an invariant forever is exactly the greatest fixpoint — sound “can hold the line” reasoning.
S7▸reachability is a least fixpoint (◊)✓
propertycanReach = least fixpoint (◊)
guaranteesThe states from which a coalition can eventually force a goal are exactly the least fixpoint — sound “can get there” reasoning.
S8▸grand-coalition determinacy ([Σ]φ ↔ ∃ successor φ)✓
property[Σ]φ ⟺ ∃ successor satisfying φ
guaranteesThe grand coalition (everyone) can ensure exactly the outcomes some successor state realizes — full control collapses to plain reachability.
composition (SB1–SB3)
SB1▸single-agent collapse → temporal reachability✓
property1-agent canReach = BFS reachability
guaranteesWith a single agent, coalitional reachability reduces to ordinary graph reachability — the strategic layer generalizes the temporal one.
SB2▸ought-implies-can (¬ability ⇒ escalate)✓
propertyoblige ⇒ discharge if canEnsure, else escalate
guaranteesOught-implies-can is enforced — an obligation the coalition cannot ensure escalates instead of being falsely discharged.
SB3▸coordination needs ability ∧ common knowledge✓
propertyexecutable ⟺ canEnsure ∧ commonKnowledge
guaranteesA joint action is executable only when the coalition both has the power and shares the knowledge to coordinate it.
Self-amendment
reflexive · 11 laws

rules that change rules, with an entrenched core that no amendment can weaken.

R1▸success (enact adds, repeal removes)✓
propertyenact adds a rule; repeal removes it
guaranteesAmendments actually take effect — enacting installs the rule, repealing retracts it.
R2▸consistency (no surviving dominated conflict)✓
propertyarbitration leaves no dominated O/F conflict standing
guaranteesAfter arbitration the rule-set is conflict-free — a dominated obligation/prohibition pair can't survive.
R3▸minimal change (enact∘repeal = id)✓
propertyenact then repeal returns the exact original rule-set
guaranteesAmendment is surgical — adding then removing a rule leaves no residue.
R4▸entrenchment (no weakening the core)✓
propertyentrenched 'safe' rule cannot be repealed or weakened, only strengthened
guaranteesTHE entrenchment law — the ring-0 floor is un-writable from within. Self-amendment can tighten the core but never loosen it.
R5▸lex superior (priority wins)✓
propertyhigher-priority rule overrides lower
guaranteesLex superior — when rules clash, the one with higher authority prevails.
R6▸lex posterior (recency breaks ties)✓
propertyequal priority ⇒ more recent rule wins
guaranteesLex posterior — among equally authoritative rules, the latest enactment governs.
R7▸arbitration idempotent✓
propertyarbitration is idempotent
guaranteesResolving the rule-set once is enough — re-arbitrating produces the same result.
R8▸reflective stability (fixpoint)✓
propertystabilize reaches a fixpoint
guaranteesIterated self-amendment converges — the system that reasons about its own rules settles, it doesn't spin.
composition (RB1–RB3)
RB1▸cannot self-permit the forbidden✓
propertyan obligation out-prioritizing an entrenched prohibition is rejected
guaranteesYou can't legislate around the floor — no amendment can grant permission to do the entrenched-forbidden.
RB2▸revision propagates to govern✓
propertyenacting a prohibition flips the live verdict (A chosen → A vetoed)
guaranteesAmendments take effect on the very next decision — the governance verdict reflects the revised rule-set immediately.
RB3▸entrenched safety survives in supervise✓
propertyentrenched temporal floor can't be repealed and still enforces
guaranteesAn entrenched safety invariant resists repeal and keeps catching trajectory violations downstream in supervision.

Where the laws bend — by design

A governance algebra has to know the difference between regimes. So the harness also checks, on every run, that certain properties fail exactly where they should. These aren’t bugs — they’re the distinctions that make the kernel honest.

H6 · idempotence
holds under the tropical dioid; fails under probability and log semirings — expected, because those aren’t idempotent. Choosing the wrong semiring is a category error the laws catch.
factivity · T
knowledge (S5) is factive in 100% of cases; belief (KD45) believes a falsehood in ~30% — the whole point of separating “knows” from “believes.”
coalition power
the grand coalition can reach what a soloist can in 100% of games, and strictly more in 25% — ought-implies-can has teeth.
affine use
spend a depletable resource three times and tokens go 3 → 0; a reusable skill stays 1 → 1 — the “of course” modality, copyable where consumables are not.