Keywords: behavioural specification; Allium v3; Bend 2; refinement; assume-guarantee; proof-carrying artifacts; PADST; deterministic simulation; TigerBeetle; reconciliation; HTMX; Elm; Datastar; CI provenance; recoverability; mutation adequacy; assurance quality.

Central objective. $\mathit{Implementation}\sqsubseteq\mathit{Specification}$: every observable implementation trace must be permitted by the approved behavioural specification.

1 Research scope and provenance

1.1 Method and version discipline

This public edition presents a generic architecture for proof-driven delivery across multiple repositories. It retains the original author’s technical thesis, mathematical distinctions and worked examples, while replacing organization-specific infrastructure and evidence with explicit architectural roles. Public language and platform references are dated research sources; implementations must pin the exact versions they use.

The examples use Allium v3 and Bend 2. Historical v2 references provide migration context. Language versions must not be silently mixed. [1–3]

1.2 Architectural roles and evidence scope

In this paper, PADST means protocol-aware distributed systems testing, and the simulation harness is a proposed controlled execution environment. These are capability descriptions, not claims that any named product already provides the complete design. A real handler behind a simulated dependency, a bounded model proof and a production observation are different evidence classes.

Financial workflows make identity, conservation and recovery requirements concrete, but the delivery architecture also applies to other distributed software systems. The arithmetic example sources are included for inspection and independent checking. Private repository inventories, operational observations and implementation-specific reproduction instructions are not part of this public edition. Consequently no such results are attributed to Abakuc or presented as publicly reproducible evidence.

1.3 Reading map

All diagrams describe proposed architecture. The appendix contains a small self-contained arithmetic model; the other configuration and UI listings are illustrative. The local example-check report states exactly what was rerun for this edition.

1.4 Corpus baselines and language migration

A corpus audit should pin the source inventory and parser/checker versions, then report parse diagnostics, checker errors and warnings separately. A parser may recover from errors while returning a zero process exit status, so successful process termination alone is not sufficient evidence of valid source.

Count authored rules and invariant blocks separately from validated obligations. Record explicit language versions, keep new pilots out of a frozen baseline denominator, and reject unsupported or invalid source before proof generation. Do not weaken failing specifications to manufacture coverage. Publish the permitted corpus and its digests when reporting empirical results.

2 Five distinct assurance classes

An evidence bundle must state what its result means. A green indicator without a subject, scope and assumption set is not a useful assurance claim. The five classes below are separate dimensions of evidence, not scores that can be added together or an automatic ladder.

2.1 Scope is part of the result

A receipt must identify the model, implementation, observation function, environment, exploration bounds, and exact candidate artifacts. “Model proven; adapter tested” is a valid composite statement. “System proven” is not a valid abbreviation for it. Missing evidence is unknown, not success. A timeout means the requested result was not obtained; it does not refute the theorem and cannot satisfy a promotion obligation.

A deterministic generator is useful because identical approved inputs produce identical outputs and reviewable diffs. Determinism alone says nothing about semantic correctness: a consistently wrong translator is still deterministic. Verified translation requires a preservation theorem for the language subset, source and target semantics, and compiler passes in the stated trust boundary.

Policy consequence. Each obligation declares required assurance classes. A weaker class may accompany a result but must not silently replace a stronger required class. An approved degraded manual release remains explicitly degraded.

3 Formal objective and trace semantics

Model component behaviour as M = (S, $S_0$, Events, $\delta$, O), with state space S, initial states $S_0$, transition relation $\delta$ and observation function O. Internal implementation actions may be hidden or represented as stuttering. The specification defines a language of permitted observable traces; financial effects, authorization outcomes and user-visible commitment claims must not be hidden by O. Refinement mappings provide a disciplined way to relate concrete state and steps to an abstract machine. [4, 5]

$$\begin{equation} \begin{aligned}\mathit{Implementation}&\sqsubseteq\mathit{Specification}\\\operatorname{Traces}(O(\mathit{Implementation}))&\subseteq\operatorname{AllowedTraces}(\mathit{Specification})\end{aligned} \end{equation}$$

3.1 What a proof must discharge

An invariant proof establishes its base case and preservation for every permitted modeled transition. A refinement argument additionally relates initial states, each concrete step to an allowed abstract step or stutter, and the observation functions. Infinite-trace liveness needs its own argument; a finite collection of successful executions cannot establish eventual completion for all executions.

$$\begin{equation} I(s_0)\;\land\;\forall s,e,s^{\prime}.\;\bigl[I(s)\land\delta(s,e,s^{\prime})\Rightarrow I(s^{\prime})\bigr] \end{equation}$$

For an intentionally changed business contract, refinement to the old specification may be inappropriate. The law delta must first be approved; the candidate is then judged against the new pinned contract and its compatibility obligations. Preconditions, units, observation projections and assumptions are part of that semantic delta, even if the JSON schema did not change.

3.2 Linearizability and financial identity

Linearizability requires completed concurrent operations to admit an equivalent sequential history that respects real-time precedence, with each operation taking effect between invocation and response. It is a property of an object’s specified operations, not a blanket property of a microservice estate. A timed-out operation may have taken effect; an admissible completion of its pending history must be considered. [6]

For a financial command, define the abstract effect, its stable business identity and the authority that linearizes it. An HTTP acknowledgement, queue delivery or DOM update is not automatically the linearization point of ledger commitment. The adapter must relate a durable ledger result to the domain observation and distinguish Submitted, OutcomeUnknown and Committed.

3.3 Non-vacuity

Prove or demonstrate feasible preconditions and exercise positive witnesses. A model that rejects every transfer may satisfy “no unauthorized transfer” while failing the business journey. Protect observation functions and require completeness checks on traces: an empty observation stream must not make a system with missing telemetry appear conformant.

3.4 A constructed observation function

For the arithmetic example, define $O_m(s)=(s.source,s.destination,e(s))$, with $e=1$ in Committed and $e=0$ in Pending or Rejected. The executable demonstration returns $(25,125,1)$. This projection distinguishes a financial effect from rejection, but only represents one operation and cannot establish a real ledger history.

The composed reference experiment therefore observes $(a,l,p,b_s,b_d,J)$: authorization state, ledger-control state, visible projection, both account balances and the complete ordered financial journal. Journal records retain operation and transfer identity, amount and asset; order and multiplicity are preserved. Financial observation in the idempotency equation means $(b_s,b_d,J)$, not merely the net balance. Expected records are independently derived from source transitions, while actual records are read from the participants’ stored state. Replies are compared separately on every step.

The observation footprint is executable: a duplicated posting changes $J$; a debit followed by an offsetting reversal also changes $J$ despite unchanged net balance; either individual account perturbation changes the observation. These negative controls guard against accidental erasure. They do not prove completeness of the chosen business vocabulary, and the reference participants are not production adapters.

4 Assume-guarantee composition

For component i, $A_i$ states assumptions about its inputs and environment; $G_i$ states its guarantees; $O_i$ defines externally visible behaviour. A local argument establishes $A_i$ $\Rightarrow$ $G_i$ under that component’s semantics. For every connected pair i,j, define $C_{ij}$: the producer’s observable guarantees, transport semantics and adapter mapping satisfy the consumer’s assumptions. [7]

$$\begin{equation} \left(\bigwedge_i G_i\right)\land\left(\bigwedge_{e\in H} C_e\right)\land\left(\bigwedge_{K\in\mathcal K}J_K\right)\land E\;\Rightarrow\;P_{\mathrm{system}} \end{equation}$$

This is the desired system obligation, not a theorem obtained by merely listing green repositories. Each premise must be discharged or explicitly retained as an environmental assumption. In cyclic systems, naïve circular reasoning is invalid: use a sound compositional rule, suitable induction or progress argument, and justified fairness conditions. Pairwise compatibility alone may miss a joint invariant such as two consumers spending the same shared resource. [7]

Producer output schemas must be compatible, but schemas are only one part of $C_{ij}$. A consumer expecting committed events is incompatible with a producer that now emits acceptance events under the same field names. A version, unit, tenant scope, ordering or idempotency change can invalidate an edge without changing its transport encoding.

4.1 A non-circular composition rule

Here $H$ is the set of compatibility hyperedges, including ordinary producer–consumer pairs and joint shared-resource obligations. Partition the dependency graph into strongly connected components $\mathcal K$. Verify each cyclic component as one joint product transition system: establish its initial invariant and preservation under every internal step and every permitted incoming action. $J_K$ records these joint obligations. Internal component guarantees cannot be assumed to establish themselves. The condensation graph is acyclic; discharge incoming assumptions in its topological order from already established predecessor guarantees and explicit environmental premises. Finally prove the displayed entailment to the system property. Acyclic singleton components use the ordinary local rule.

This rule is deliberately conservative: a large cycle may require a large product proof, or a reviewed coarser abstraction with a refinement argument. A cyclic drawing is not a circular proof. Pairwise schemas do not discharge resource hyperedges. The runnable control example includes a counterexample with only 100 source cents: two independently approved 100-cent postings satisfy every local finite-control invariant but produce a source balance of $-100$. Here $-100$ is a derived spend position, never a negative TigerBeetle counter. The joint liquidity invariant rejects that trace. The main experiment instead declares 250 source cents and two possible postings; that fixed bound must not be generalized to arbitrary liquidity.

5 A realistic repository decomposition

The repository is a delivery boundary; the semantic component is a proof boundary. One repository may export several contracts, and a journey may cross many repositories. The following decomposition is illustrative, using generic capability names—not a claim that each row is already a separately verified product.

A specification repository owns approved intent and governance artifacts. A delivery controller owns workflow execution, independent obligation resolution and evidence gates. Shared libraries can host reusable semantic/protocol machinery; the system-verification repository composes the result. Ownership must be explicit for interfaces that span these roles.

5.1 The dependency and proof graph

Figure 1 maps selected behavioural obligations across the repositories and into system verification.

5.2 Compatibility is behavioural

Consider a command path UI $\rightarrow$ API $\rightarrow$ policy $\rightarrow$ money domain $\rightarrow$ ledger adapter. The UI supplies a stable operation identity, but the API authenticates and validates it. Policy guarantees an authorization decision bound to the same command hash and policy version. The domain assumes that binding when constructing its transition. The adapter guarantees that retries encode the same TigerBeetle transfer identity and do not substitute a new payload.

On the return path, a CDC event must denote the same aggregate and operation, a projection must preserve versions, and a fragment or patch must not advertise a stronger state than its durable observation. A contract edge therefore contains identity mapping, units, cardinality, rejection behaviour, ordering scope, and an observation mapping—not just a schema reference.

5.3 Shared constraints and graph cycles

Use hyperedges when an obligation depends on several producers, such as an FX quote plus both liquidity accounts and an authorization receipt. Condense strongly connected components for impact planning; do not mistake that graph operation for a proof that cyclic assumptions hold. Joint conservation and approval-before-execution laws live in the system layer even when all local schemas validate.

Contract metadata must identify dependencies on policy, account mapping, numeric scales, observation functions and infrastructure. Missing edges are assurance defects: a supposedly small change cannot be declared independent because the graph forgot its consumers.

6 From Allium v3 to Bend 2

Allium v3 describes entities and rules using triggers, preconditions and postconditions, with separate non-normative guidance. Its reference distinguishes rejection of an external stimulus from non-firing of a temporal trigger and termination of a chained trigger. A translator must preserve those distinctions rather than imposing an invented global rollback rule. [3]

6.1 Deterministic behavioural IR

The proposed translator emits typed state and event vocabularies, transition relations, preconditions, postconditions, invariants, permitted traces, and observation functions. Every obligation retains its source rule ID and span, normalized specification hash, transitive imports, assumptions, numeric units, asset scales, overflow and rounding rules, and temporal interpretation. Canonical serialization and pinned generator inputs make the IR reproducible.

An unsupported or ambiguous expression is an explicit unresolved obligation. Undefined predicates, unresolved domain questions, unbounded temporal requirements and implicit unit conversions must not become assumed truths. A language-version mismatch fails before proof generation. The examples now explicitly select v3; the previous v2 edition is not evidence for a v3 corpus. Corpus conformance must be checked before generation. [2]

6.2 Bend’s contribution and its limits

Bend 2 separates laws from their proofs through LAWS.bend and PROOF.bend; its dependent type checker checks proof terms. Termination restrictions support the proof discipline, while @unsafe permits behaviour outside the associated guarantees. Foreign code, axioms and dependencies require an explicit inventory. [8]

Upstream states that the compiler is not fully audited and that its Lean formalization and implementation differ. A pinned checker reduces drift; it does not eliminate the trusted computing base. The proposed bridge must not advertise audited end-to-end soundness that its toolchain has not established. [9]

6.3 Runnable Allium v3 and Bend 2 example

The following example is supplied for checking with Allium CLI 3.0.3 (language version 3) and Bend 2.0.16. It models one isolated USD operation, in integer cents, using a terminal result to make retries idempotent. The concrete fixtures start with 125 cents in the source and 25 cents in the destination; a 100-cent command yields 25 and 125 cents, including after a retry. These are reproducible test data, not production customer transactions. The Allium checker release supports language versions 1, 2 and 3; the file explicitly selects version 3. [10]

What the checks mean. Allium validates the specification’s syntax and static references; it does not execute these rules or prove their invariants. Bend checks six universally quantified laws of the supplied natural-number model: reservation conservation, transfer conservation, duplicate-submit idempotency, retry state preservation, the terminal-state retry guard, and observation stability. Concrete fixtures and deliberately invalid variants can exercise the checkers. The build report for this edition names the checks actually executed. The complete model and proof terms are printed in the appendix ; editable source files are maintained separately in the research repository.

Listing 1. Complete Allium v3 specification, accepted by Allium CLI 3.0.3. Its invariants are declared intent, not theorems proved by Allium.

-- allium: 3

enum Phase { pending | committed | rejected }
entity Payment {
    operation_id: String
    asset: String
    amount: Integer
    initial_source: Integer
    initial_destination: Integer
    source: Integer
    destination: Integer
    phase: Phase
}
given { payment: Payment }

rule CommitPayment {
    when: SubmitFunded(operation_id, amount, asset)
    requires: operation_id = payment.operation_id
    requires: amount = payment.amount
    requires: asset = payment.asset
    requires: payment.phase = pending
    requires: amount >= 0
    requires: payment.source >= amount
    ensures: payment.source = payment.source - amount
    ensures: payment.destination = payment.destination + amount
    ensures: payment.phase = committed
    ensures: payment.operation_id = payment.operation_id
    ensures: payment.asset = payment.asset
    ensures: payment.amount = payment.amount
    ensures: payment.initial_source = payment.initial_source
    ensures: payment.initial_destination = payment.initial_destination
}

rule RejectInsufficientFunds {
    when: SubmitUnfunded(operation_id, amount, asset)
    requires: operation_id = payment.operation_id
    requires: amount = payment.amount
    requires: asset = payment.asset
    requires: payment.phase = pending
    requires: amount >= 0
    requires: payment.source < amount
    ensures: payment.source = payment.source
    ensures: payment.destination = payment.destination
    ensures: payment.phase = rejected
    ensures: payment.operation_id = payment.operation_id
    ensures: payment.asset = payment.asset
    ensures: payment.amount = payment.amount
    ensures: payment.initial_source = payment.initial_source
    ensures: payment.initial_destination = payment.initial_destination
}

rule RetryPayment {
    when: Retry(operation_id, amount, asset)
    requires: operation_id = payment.operation_id
    requires: amount = payment.amount
    requires: asset = payment.asset
    requires: payment.phase != pending
    ensures: payment.source = payment.source
    ensures: payment.destination = payment.destination
    ensures: payment.phase = payment.phase
    ensures: payment.operation_id = payment.operation_id
    ensures: payment.asset = payment.asset
    ensures: payment.amount = payment.amount
    ensures: payment.initial_source = payment.initial_source
    ensures: payment.initial_destination = payment.initial_destination
}

invariant Conservation {
    payment.source + payment.destination =
        payment.initial_source + payment.initial_destination
}

invariant NonNegativeBalances {
    payment.source >= 0 and payment.destination >= 0
}

surface PaymentCommands {
    facing item: Payment
    exposes: item.phase
    provides:
        SubmitFunded(operation_id: String, amount: Integer, asset: String)
        SubmitUnfunded(operation_id: String, amount: Integer, asset: String)
        Retry(operation_id: String, amount: Integer, asset: String)
}

Listing 2. Actual Bend 2 laws. The paired PROOF.bend discharges all six without unsafe annotations or unresolved proof holes in the example sources.

import Base
import ./Payment.bend as Payment
import ./Balance.bend as Balance

law reservation_conserves:
  for amount: Nat
  for source: Nat
  Balance.Conserves(Balance.reserve(amount, source), amount, source)

law duplicate_submit_idempotent:
  for +amount: Nat
  for state: Payment.Payment
  {Payment.apply(amount, Payment.apply(amount, state)) ==
   Payment.apply(amount, state) : Payment.Payment}

law transfer_conserves:
  for +amount: Nat
  for state: Payment.Payment
  {Payment.total(Payment.apply(amount, state)) ==
   Payment.total(state) : Nat}

law retry_preserves_state:
  for state: Payment.Payment
  {Payment.retry_state(Payment.retry(state)) == state : Payment.Payment}

law retry_requires_terminal:
  for state: Payment.Payment
  {Payment.retry_accepted(Payment.retry(state)) == Payment.terminal(state) : Bool}

law observed_retry_stable:
  for +state: Payment.Payment
  {Payment.observe(Payment.retry_state(Payment.retry(state))) ==
   Payment.observe(state) : Payment.Observation}

Listing 3. Executable submit-then-retry demonstration, with a structured financial observation.

import Base
import ./Payment.bend as Payment
import ./PROOF.bend as Proof

def main() -> Payment.Observation:
  Payment.observe(Payment.retry_state(Payment.retry(
    Payment.apply(100n, Payment.Pending{125n, 25n}))))

From the paper directory, use the example-check command below with installed Allium 3.0.3 and Bend 2.0.16 binaries. The command records tool versions, source digests and actual results; no result is inferred from the presence of a proof file.

Listing 4. Check the included arithmetic example with explicit local tool paths.

ALLIUM=/path/to/allium BEND=/path/to/bend \
  python3 check_examples.py

The report is an unsigned local reproducibility record. It is not a deployment attestation, an independent review or a proof about a production adapter.

Boundary. This arithmetic Bend model remains manually written against selected Allium intent. The finite-control profile discussed below is separate and does not cover this Integer/arithmetic specification and is not a verified translator. One operation identity, matching payload, asset and account mapping, non-negative initial balances, and sequential atomic execution are assumptions at this projection boundary. The Allium preconditions state identity/payload matching; Bend’s single-operation state does not implement ID lookup, payload hashing or authorization. Natural numbers avoid fixed-width overflow in the model but do not establish machine-integer or asset-scale correctness in an adapter. Zero-sized commands are allowed by this pedagogic model; it is not an executable TigerBeetle API specification. There is no network, concurrency, persistence or bank integration in this example.

The implementation relation must include error paths, serialization and observable effects. A proof of a copied pure function cannot cover a handler that bypasses it, converts amounts differently, or trusts a UI permission signal. Reachability and adapter evidence belong in the binding.

6.4 Obligation coverage and the retry distinction

Typing and explicit proof terms are different discharge techniques within the same formal-model assurance class. A Nat representation does not upgrade an unverified Integer-to-Nat adapter to verified implementation. The four boundary controls test selected invalid inputs; they do not prove that all external adapters enforce this conversion.

Bend’s +amount annotation permits reusable access to a Data value. It does not mean a positive number and does not narrow Nat: zero remains included. The reservation law needs a single use; laws that reuse an amount bind it with +. All six laws quantify over their stated types under the checker assumptions.

6.5 A bounded finite external-event profile

A candidate compiler profile allium3-finite-external-v1 consumes the official v3 AST, source bytes and an explicit initial valuation. It accepts one owned entity and one binding; enum-valued state and event parameters; equality, inequality, conjunction and disjunction guards; and simultaneous pre-state assignments to every field. Each external event has exactly one rule. Every frame assignment is explicit. It rejects parser error diagnostics even if the parser process exits zero.

The profile rejects imports, Integer arithmetic, temporal triggers, chained triggers, implicit frames, conditional effects and ambiguous dispatch. External precondition failure returns the unchanged state and a rejected reply. This rule is not applied to unsupported trigger kinds. There is no claim to translate the full Allium language or an arbitrary specification corpus.

Bounds are six state fields, eight values per enum, 256 states, 128 parameter valuations per event and 8,192 transition rows; predicate depth is at most six. Recursive predicate processing decreases AST depth. Enumeration visits finite Cartesian products; emitted Bend functions use finite case analysis without recursive transition evaluation. These bounds give a termination argument and explicit rejection before an unbounded expansion, not a proof of semantic preservation.

Every rule, requires clause, ensured field and invariant has an IR coverage entry. Enabled rules and effects require an admissible witness, preventing impossible preconditions from passing silently. Source spans and source hashes retain provenance; the semantic hash excludes source locations but includes initial state and transition meaning. A compiler library does not itself prove that a supplied AST corresponds to supplied bytes: the driver runs the pinned parser and records both.

A validation programme should exercise independent authorization, ledger-control and monotonic-projection examples. An independently implemented source interpreter should construct expected transitions directly from the parsed source. Generated step and accepted-reply results should be compared against those expectations for every row in the declared finite input universe.

Publish the number of states, parameter valuations, transition rows, generated obligations, unsupported constructs and rejected mutants for each example. Repeated generation should produce identical bytes under pinned inputs. This establishes evidence about those finite instances; it does not establish a general compiler-correctness theorem.

Maintain one canonical owner for compiler code and one for approved specifications. A public replication archive must include the permitted source, tool identities and actual output before its measurements can be presented as independently reproducible results. This edition does not distribute an organization-specific compiler or its private corpus.

7 Proof-carrying component artifacts

Every component repository publishes immutable evidence tied to its source and built subject. This illustrative record satisfies the basic interchange requirements; a production schema must additionally encode assurance class, applicability, observation hash, trust closure, timestamps and signer identity. A signature authenticates an assertion’s origin and subject—it does not make an incorrect assertion true. [11, 12]

Listing 5. Illustrative evidence schema; placeholders are not real verification results.

component: ledger-adapter
source_sha: <full-commit-sha>
artifact_digest: sha256:...
contract:
  name: money-transfer
  version: 4
contract_ir_hash: sha256:...
assumptions:
  - authorized-command.v2
  - unique-operation-id.v1
  - account-mapping.v3
guarantees:
  - single-ledger-conservation.v3
  - retry-idempotency.v2
  - stable-observation.v1
observations:
  - TransferAccepted
  - TransferRejected
  - TransferCommitted
proof:
  checker: bend
  checker_version: <pinned-version>
  laws_hash: sha256:...
  proof_hash: sha256:...
  result: pass
unsafe_axioms: []
test_evidence:
  padst_trace_digest: sha256:...
  simulation_scenario_digest: sha256:...

The system verifier resolves the signed subject digest, checks signer/workflow identity, validates the schema and expiry, compares the declared obligation set with its independently resolved set, and checks the full dependency closure. Non-Bend repositories must declare their actual assurance method or an approved not-applicable scope; they must not manufacture a Bend pass merely to populate this schema.

7.1 Freeze intent; then bind the candidate

Two snapshots prevent a circular lifecycle. An obligation snapshot freezes approved intent, assumptions, required assurance classes, bindings, scope and baseline policy before an agent changes code. A candidate snapshot records the exact produced source, model, proof, configuration and artifacts after the work. Demanding final proof hashes before writing the code would make the workflow impossible.

7.2 The deployable unit is a locked system manifest

Listing 6. Illustrative manifest skeleton, not a deployment-ready configuration.

system_manifest:
  baseline_manifest: sha256:...
  components:
    ledger-adapter:
      source_sha: <full-commit-sha>
      artifact_digest: sha256:...
      contract_version: money-transfer.v4
      contract_ir_hash: sha256:...
      proof_hash: sha256:...
    # Every other participating component has an exact entry.
  compatibility_proofs: [sha256:...]
  padst_scenario_set: sha256:...
  padst_evidence: sha256:...
  simulation_scenario_evidence: sha256:...
  infrastructure_version: <immutable-version-and-digest>
  deployment_policy_version: <immutable-version-and-digest>
  verifier_workflow_sha: <full-commit-sha>

Hash a canonical manifest representation. References must resolve to immutable content, including browser bundles and schemas. Never prove a composition assembled from moving branch heads. Preserve old receipts as historical facts; invalidate their applicability to a changed candidate rather than rewriting their recorded outcomes.

8 Change-impact analysis

When repository k changes, compare its exported semantic contract with the approved baseline. The impact classifier examines internal implementation, exported schemas, behavioural semantics, preconditions, guarantees, observation functions, event ordering, identity/idempotency semantics, units and asset scales, authorization policy, and infrastructure assumptions. Paths and dependency files are inputs, not sufficient semantic evidence.

8.1 Selective recomputation

Within the affected proof closure, rerun local component proofs, repository-edge compatibility proofs, affected end-to-end trace laws, PADST protocol scenarios, controlled simulations, and relevant browser and ledger integration tests. Cache reuse requires equality of all relevant semantic and trust inputs, not merely a matching contract version string. An unchanged theorem can be reused only with an established binding to the newly built implementation.

The system verifier issues four separate assertions: component safety for k; compatibility of the affected edges; end-to-end trace refinement for affected journeys at the actual evidence class; and validity of one exact deployable manifest. If the implementation connection is only tested, the third assertion is tested trace conformance—not a universal trace-refinement proof.

Review example. Changing a projection’s version comparison from “strictly newer” to “arrival order” affects CDC $\rightarrow$ projection $\rightarrow$ SSE $\rightarrow$ UI even when every field and endpoint is unchanged.

8.2 Closure cost and reuse limits

Compute the affected closure over both old and new dependency graphs so that deleted edges cannot hide impact. Report local obligations, downstream consumers and mandatory manifest validation separately. Graph size alone does not establish verification savings.

With adjacency lists, reachability and strongly connected component condensation cost $O(|V|+|E|)$. Discharging the resulting obligations may dominate that cost: joint state spaces multiply, theorem checking has its own complexity, and a shared semantic or toolchain change can invalidate a broad closure. Measure those costs on an explicitly published corpus rather than extrapolating from a private pilot.

Separate semantic theorem reuse from artifact binding and receipt reuse. Unchanged semantic inputs may permit reusing a theorem; changed implementation bytes still require binding evidence and new manifest-specific authorization. A signature over the old manifest cannot be reused for a new one. Cache keys include compiler/checker identities, axioms, observation definitions and environmental profiles. Strict reuse can be expensive; partitioning contracts and naming assumptions precisely reduces avoidable invalidation without weakening these conditions.

9 PADST: testing protocol meaning

PADST is the proposed bridge from static obligations to protocols exercised by real distributed components. It operates on typed messages and protocol state, not only arbitrary byte traffic. A generator knows that a post resolves a particular pending transfer, an approval belongs to a particular payment version, or an SSE replay cursor belongs to a particular stream epoch. State-machine testing supplies a useful foundation, but its explored executions remain a sample unless completeness is separately established. [13, 14]

$$\begin{equation} \begin{aligned}\mathit{Scenario}={}&\mathit{InitialState}+\mathit{ProtocolTrace}\\&+\mathit{FaultSchedule}+\mathit{ExpectedObservations}\end{aligned} \end{equation}$$

$$\begin{equation} \mathit{ObservedTrace}\in\operatorname{AllowedTraces}(\mathit{Specification}) \end{equation}$$

PADST consumes the system proof graph, approved Allium behaviours, generated behavioural IR, state-machine definitions, protocol schemas, component assumptions and guarantees, a candidate manifest, a fault model, and protected observation functions. It first constructs feasible positive journeys, then perturbs identity, order, timing, state and dependencies. Deliberately invalid requests are legitimate inputs: rejection and absence of financial effect are expected observations, not necessarily test failures.

Related protocol-oriented work includes state-machine languages and consensus-testing DSLs. They motivate explicit protocol state and controlled adversarial scheduling; they are not citations for a public PADST product or proof that the reference platform’s proposed machinery already exists. [14, 15]

9.1 Adversarial trace obligations

9.2 A concrete scenario

Initial state: payment p is authorized, the source has sufficient constrained balance, no transfer with identity t exists, and the projection is at version 11. Send Submit(p,t), let the ledger commit, drop the response, crash the publisher, retry Submit(p,t), restart CDC, deliver its event twice, and reconnect the UI stream after rendering version 12. Expected observations include one committed transfer, a stable original result, one effective projection advance, and no return to version 11.

Check the complete observation history against the language, not only the final account balance. A final balance may look correct after an unauthorized transfer followed by a compensating transfer. The prohibited intermediate effect still matters. Preserve the first counterexample, its source observations and the causal relationships needed to reproduce it.

Meaning of a pass. A PADST pass supports conformance for the explored initial states, traces, schedules and fault bounds. It is a universal result only if exhaustive coverage and the correspondence to the implementation have themselves been established.

9.3 CDC and persistence boundaries

TigerBeetle documents CDC publication to AMQP 0.9.1 brokers with at-least-once semantics: recovery can replay a message that was delivered but not acknowledged. Consumers are responsible for idempotent processing. Event bodies retain nanosecond timestamps; the AMQP timestamp header has lower precision. Large integers are encoded as strings for interoperability. These details belong in the protocol contract and decoder tests. [16]

RabbitMQ reliability documentation makes acknowledgements and duplicate handling part of application reliability. Configure Amazon MQ/RabbitMQ assumptions explicitly; broker delivery is not end-to-end exactly-once business execution. A producer retry, consumer restart and lost acknowledgement can all expose duplication. [17]

DynamoDB conditional writes and transactions can guard authoritative records within their documented boundary. They do not create an atomic transaction with TigerBeetle. Persist stable business/ledger identities and define recovery at each cross-store step; then exercise those exact boundaries. A read model should not infer that an absent local receipt means the ledger never committed. [18]

TigerBeetle’s own safety/testing practices are valuable dependency evidence, but they do not prove the application’s codecs, mappings, queue configuration or recovery protocol. The candidate manifest and adapter tests must establish that connection separately. [19]

9.4 A newer version is not always a complete prefix

A full version-19 snapshot may supersede version 17 if its observation contract includes the intervening state. An incremental version-19 delta cannot simply skip version 18 unless the update algebra proves that safe. Track gaps separately from monotonicity. Equal versions with conflicting payloads must surface a conflict; a strict numeric comparison alone is insufficient. PADST should vary whether a message is a snapshot or delta and crash between recording the version and applying its content.

$$\begin{equation} \begin{aligned}\text{older version}&\Rightarrow\text{no regression}\\\text{equal version}+\text{different authoritative payload}&\Rightarrow\text{conflict}\end{aligned} \end{equation}$$

10 Simulation harness: controlled execution

simulation harness is the proposed controlled substrate used by PADST, not another unit-test framework. Its target is sufficient control and observation of distributed execution to replay meaningful failures against an exact manifest. Deterministic simulation has strong precedent in FoundationDB; those techniques depend on deliberate control of nondeterminism, not merely starting containers with a seed. [20, 21]

10.1 Distinguish targets from implemented coverage

A protocol runtime may execute real handlers with simulated storage, queues or ledgers. That is useful evidence but does not mean every production binary and cloud service was exercised. The exact executed paths, substituted adapters and excluded participants belong in the receipt.

Therefore the table above is a target capability contract. Each run must declare which effects were simulated, which production handlers or binaries executed, and which participants were absent. A missing node or uncontrolled effect cannot be hidden by calling the whole environment deterministic.

10.2 Execution, replay and reduction

A seed is necessary but not sufficient. Replay also fixes code and artifact versions, initial persistent state, RNG streams, event tie-breaking rules, clock domains, injected faults, dependency responses, and relevant runtime configuration. The scheduler records enough information to distinguish semantic divergence from a changed harness. Snapshot hashes and the event log identify the executed world.

Use two explicitly labelled lanes. A deterministic semantic lane runs real handlers or verified cores with controlled adapters. An exact-artifact lane runs the candidate binaries with an execution substrate capable of controlling their nondeterministic inputs. If instrumentation changes the artifact, publish that relationship and the instrumented digest; do not claim the production digest was executed. Real cloud/browser integration outside sufficient control is separate empirical evidence.

10.3 Minimize without changing the failure

Reduce events, inputs and faults while preserving protocol feasibility, the same manifest, and the failing property. Re-run every reduction and retain the original trace. A small failure that cannot be replayed is not a replacement for the original witness. Record/replay research shows that faithful interception boundaries matter; a process recorder alone does not reproduce an entire distributed environment. [22]

Targeted fault selection can use dependency/causal information rather than uniform random faults. Lineage-driven fault injection provides a relevant precedent, but its bounded guarantees must not be generalized into unlimited production assurance. [23]

10.4 The empirical assurance boundary

The following claims require observations from the exercised implementation paths, with explicit scenario and fault bounds. They are not consequences of a simulator reporting success alone.

What they cannot establish unconditionally

Neither framework can determine that the approved specification expresses the right business intent; that every possible production fault was included; or that an external SaaS/cloud dependency always respects its contract. A non-exhaustive test set does not prove universal correctness. A correctly bound rate snapshot does not prove a commercially supplied FX rate is economically correct. No finite campaign establishes unconditional availability.

Likewise, semantic DOM correctness does not imply correct pixels, accessibility or usability. Browser testing must still evaluate focus, keyboard interaction, announcements, layout and real event behaviour. Security, performance and recovery claims need their own workloads and assumptions.

Coverage denominator. Report obligations checked / required, real handlers or artifacts exercised / required, adapters simulated / real, seeds and schedules explored, fault bounds, and unresolved gaps. A green result with an unspecified denominator is not a system claim.

10.5 Conditional liveness and a progress certificate

Safety excludes forbidden effects; payments also require progress obligations. Write $\operatorname{Accepted}(o)\rightsquigarrow\operatorname{Settled}(o)\lor\operatorname{Escalated}(o)$ under explicitly named recovery, delivery and decision assumptions. Escalation is an accountable terminal outcome, not evidence that the money arrived. Actual settlement additionally assumes the external rail accepts and eventually processes the instruction.

For an illustrative composition with two operations, define rank $R=u+2(2-p)+p-v$, where $u$ is the number lacking approval, $p$ the number posted, and $v$ the visible aggregate version. Initially $R=6$. A checker should verify nonnegative rank, non-increase on every edge, a decreasing enabled action at every nonterminal state, and persistence of the enabled progress set across rank-preserving edges. Under weak fairness for those continuously enabled progress actions, rank reaches zero within at most six progress actions. A bound of $6B$ total steps additionally requires a progress action within every $B$ steps.

Without fairness the infinite schedule drop, drop, ... is a counterexample; a validation harness should retain this repeating trace. Checking a finite graph certificate with a source interpreter is distinct from proving an infinite-trace theorem in Bend. Unbounded queues, failing banks, expired authorization and production recovery are outside it. Each real journey needs its own progress obligation and assumption monitoring, alongside its safety proofs.

11 Money example I: a basic transfer

Let a command carry tenant, operation ID, debit account, credit account, ledger, positive integer amount and canonical payload hash. Each account stores four unsigned counters: posted debits $D^p$, posted credits $C^p$, pending debits $D^u$, and pending credits $C^u$. TigerBeetle counters and amounts are uint128; the mathematical model must separately discharge overflow bounds. A derived signed position is $q_a=C^p_a-D^p_a$. It is not a stored negative counter or a universal account-normal balance. [24, 25]

For an ordinary posted transfer of $m>0$ from debit account $d$ to credit account $c$, the only counter changes are $D^{p\prime}_d=D^p_d+m$ and $C^{p\prime}_c=C^p_c+m$. The signed conservation equation follows from that representation:

$$\begin{equation} \begin{aligned}q_d^{\prime}&=q_d-m,&q_c^{\prime}&=q_c+m,\\\sum_{a\in\operatorname{ledger}(l)}q_a^{\prime}&=\sum_{a\in\operatorname{ledger}(l)}q_a.\end{aligned} \end{equation}$$

The conservation proof sketch is cancellation of $-$m and +m. For a credit-funded debit account the reservation-aware requirement is $D^p_d+D^u_d+m\leq C^p_d$; pending credits cannot fund the transfer. Apply the actual account-normal definition: TigerBeetle keeps debit and credit counters and supports configurable balance constraints; a single unsigned “balance” is not a faithful model of every account type. [24, 25]

Machine-checked obligations must cover per-asset conservation, account/ledger compatibility, constrained available balances including pending reservations, atomic movement, stable transfer identity, and at-most-one committed financial effect. The arithmetic argument above is a model derivation, not a claim that this paper executed a Bend proof of the production adapter.

Atomic movement here means the two sides of the ledger transfer commit together. It does not assert an atomic transaction across TigerBeetle, a bank rail, a workflow database and a browser. Those are separate protocol boundaries.

11.1 Timeouts, retries and pending funds

Stable identity is the essential bridge

Record or derive a stable transfer ID for the business operation and reuse the same command fields on retry. TigerBeetle’s reliable-submission guidance treats application-level retry identity as essential; generating a new ID after an uncertain result can create another valid transfer. Duplicate-result handling must also distinguish a matching existing transfer from an ID collision or conflicting payload. [26, 27]

Pending transfers are not mutable records

TigerBeetle pending transfers reserve funds without posting them. Posting, voiding and expiration resolve that reservation; resolution uses a new transfer referring to the pending ID. A pending transfer can be resolved only once. A partial post posts the selected amount and releases the remainder; it is not a reusable reservoir for repeated partial posts. The original transfer remains immutable. [28]

For a 10000-unit reservation partially posted for 6000, the remaining 4000 is released. A second post against the same pending transfer must not be used to consume it later. If the business needs staged capture, model separate reservations or a different explicit protocol. PADST must explore post/void races, expiration, retry of the resolution transfer and restart between observing the ledger and persisting the workflow result.

Proof sketch for retry idempotency

$$\begin{equation} \operatorname{financialObs}(\operatorname{apply}(\operatorname{apply}(s,c),c))=\operatorname{financialObs}(\operatorname{apply}(s,c)) \end{equation}$$

The abstract transition returns the stored outcome when the scoped identity and canonical payload already exist. Prove the first successful application records that identity atomically in the modeled authority; later identical applications preserve the financial projection. Real persistence, cross-store recovery and ID-retention assumptions must then be discharged by the implementation relation and integration evidence.

11.2 Pending and posted are separate ledger states

For a reservation $r>0$, increment $D^u_d$ and $C^u_c$ by $r$, leaving both posted counters unchanged. Resolving it with a post amount $0<p\leq r$ removes the full $r$ from both pending counters and adds only $p$ to the corresponding posted counters. Thus a partial post releases $r-p$; it cannot be posted a second time. A void removes the reservation without changing posted counters. An explicit post or void appends a new transfer referencing the pending ID; the original transfer is immutable. Expiry releases the reservation when processed, and its observed counter release may lag the deadline. [27, 28]

$$\begin{equation} \begin{aligned} \text{reserve }r:\quad&D^{u\prime}_d=D^u_d+r,& C^{u\prime}_c=C^u_c+r,\\ \text{post }p:\quad&D^{u\prime}_d=D^u_d-r,& C^{u\prime}_c=C^u_c-r,\\ &D^{p\prime}_d=D^p_d+p,& C^{p\prime}_c=C^p_c+p. \end{aligned} \end{equation}$$ The subtraction releases an existing reservation; it never permits negative counters. Both legs of a linked payout have pending debit and pending credit entries. Linked chains must cover the reservation and resolution operations separately. A batch alone is not atomic, and a chain ends with linked=false. [29]

Ledger adapter units. The arithmetic fixture uses cents. An illustrative adapter using a $10^7$ scale would represent GBP 100.00 as 1,000,000,000 ledger units rather than 10,000 pence. Currency identity and numeric scale are separate mappings. Check each conversion before encoding a real ledger request; the earlier figures are explanatory minor-unit examples, not production payloads.

12 Money example II: reconciliation

Reconciliation relates three bounded populations: B, business/control-plane operations; T, TigerBeetle transfers; and X, external bank or processor records. Define deterministic matching over operation ID, transfer ID, asset, integer amount, direction, account mapping, settlement reference and source high-water mark. A duplicate or ambiguous key is an exception, not permission to select an arbitrary match.

$$\begin{equation} \begin{aligned} \forall b\in\operatorname{Posted}(B):\;&\exists!c\in\operatorname{Outcomes}(b).\;\operatorname{valid}(c),\\ \operatorname{Matched}(b)\;&\Rightarrow\exists!t\in T.\;\operatorname{match}(b,t),\\ \forall t\in\operatorname{InScope}(T):\;&(\exists b\in B.\;\operatorname{match}(b,t))\lor\operatorname{classified}(t). \end{aligned} \end{equation}$$

Uniqueness applies to the classification at an immutable snapshot cut. A duplicate yields one Duplicate outcome retaining all candidates, not a fabricated unique match. The Matched branch requires exactly one transfer for a one-leg operation. Expand FX, fees and corrections into ExpectedLegs before applying that branch. Administrative closure additionally requires every outcome to be Matched or Escalated; classifying a discrepancy alone does not close it.

“Classified” means a permitted, versioned classification with provenance and an accountable disposition, such as an identified correction or an escalated orphan. It is not a catch-all predicate that can be set true to satisfy the equation. External completeness additionally requires each in-scope settled leg to have its expected X association or a declared timing difference/escalation.

12.1 Completeness needs an immutable cut

Seal these inputs before claiming completeness. TigerBeetle historical balance queries require the relevant account history capability; capture the account configuration and pagination/cut semantics. Automatic pending-timeout expiry is not a new historical-balance entry, so a historical row is not a universal pending-state snapshot. A current balance alone cannot show that every expected transfer was reconciled. [25, 30]

12.2 Reconciliation lifecycle and faults

Unseen items become Matched, TimingDifference, AmountDifference, MissingInternal, MissingExternal or Duplicate. Unresolved discrepancies move to Escalated with owner, reason and follow-up. A window may close administratively only when every in-scope item is matched or explicitly escalated. “Closed with exceptions” must remain distinct from “all funds matched.” A late correction creates a linked amendment or a new window; it does not rewrite the original completeness receipt.

The proof target is the matching/classification algorithm over the declared finite snapshots, including uniqueness and closure accounting. It does not prove that an external institution supplied all reality. PADST exercises the protocol obtaining those cuts; the simulation harness replays the precise failed schedule, including delayed publication and record arrival.

12.3 Reconcile all four counters without spending pending credits

A posted trial balance is only one control. For a complete closed ledger population $L$ at a consistent cut, require both: $$\begin{equation} \sum_{a\in L}D^p_a=\sum_{a\in L}C^p_a, \qquad \sum_{a\in L}D^u_a=\sum_{a\in L}C^u_a. \end{equation}$$ These equalities neither identify the correct beneficiaries nor establish agreement with the bank. A subset such as the real-bank corridors alone need not balance; include its actual counterpart accounts or prove the boundary-flow relation. Shared edge accounts serving multiple tiers cannot be assumed to close a selected subset.

For a credit-funded corridor, distinguish the signed posted position $C^p-D^p$, the unclamped spend position $C^p-D^p-D^u$, and both gross pending counters. Compare a bank closing position with the sum of posted positions in its reviewed corridor-plus-allocation set at the declared cut. Pending reservations have their own identity, status, expiry and resolution checks. Do not mix them into the bank-closing amount to obtain equality.

During reservation the corridor has GBP 100 posted and GBP 70 spend position. Afterwards it has GBP 80 posted and no pending amount. A void instead leaves GBP 100 posted. The paired pending credit is visible throughout; an unallocated destination cannot be omitted from a reservation.

12.4 Sealed posted positions and live counters

A useful observation is $O_4(s)=(K_s,R_s,J_s)$, where $K_s$ retains all four counters per account, $R_s$ retains reservations, and $J_s$ is the resolution journal. Exercise full posting, partial posting, void and expiry separately. Reject conflicting retries, excess posts, second resolutions, unknown accounts and invalid amounts. A discrepancy that increases pending debits and credits equally can escape a net-only check; comparing all four counters exposes it.

For an illustrative reclassification policy, allocation moves value from a bank-linked pool to a project account. The bank position is the sum over a reviewed attribution set $S_c$ containing the pool and its allocated positions. Every member is counted once; sets for different bank accounts must be disjoint. For example, a bank balance of GBP 100 may correspond to GBP 75 in the pool plus GBP 25 in a project. A pool-only comparison would report false drift. $$\begin{equation} B_c(t)=\sum_{a\in S_c}\bigl(C^p_a(t)-D^p_a(t)\bigr), \qquad S_c\cap S_d=\varnothing\quad(c\neq d). \end{equation}$$

Bind membership, currency and business day into the receipt. Missing or overlapping members must fail the comparison. Arithmetic equality cannot establish the business completeness of an incorrectly approved attribution set. Keep legal entities, bank accounts and account ownership distinct even when they share a currency.

A historical posted-position collector needs a bounded, consistent source query and an explicit cutoff. Pending and void records do not themselves contribute a posted amount; a posting of a pending transfer contributes its actual amount once. Bind record hashes, counts and source identity, and fail rather than silently truncate when query limits are exhausted.

An imported-transfer timestamp barrier is one possible premise for stabilising a historical prefix under the documented TigerBeetle contract. It requires careful treatment of the cluster’s last committed timestamp and the observation cutoff; a collector must not create a financial transfer merely to manufacture that premise. This is a protocol design consideration, not a theorem supplied by this paper. [31]

Store historical posted cuts separately from current counter observations. Live pending values and expiry effects cannot be reconstructed from posted history alone. Preserve their actual observation times, and never relabel a projection-only result as a native historical observation. Validate the design against the selected ledger version before making an operational claim.

13 Money example III: foreign exchange

Tigerlings is TigerBeetle’s official exercise repository, including linked and two-phase transfers. It is useful for validating adapter understanding, not as a formal certification. The official FX recipe uses separate ledgers for currencies and a liquidity provider. Two same-ledger transfers are atomically linked; direct transfers between accounts on different ledgers are not the mechanism. [32, 33]

For 100.00 USD at the documented rate 82.42135 INR per USD, the quoted destination amount rounds to 8,242.14 INR. With two decimal places for both assets, the minor-unit amounts are 10000 and 824214. The final event has linked=false; the preceding flag links its outcome to the next event. The chain succeeds or fails as a unit within one TigerBeetle cluster. An ordinary batch is not automatically one atomic chain. [29, 33]

$$\begin{equation} \begin{aligned}\Delta\sum q_{\mathrm{USD}}&=-10000+10000=0,\\\Delta\sum q_{\mathrm{INR}}&=-824214+824214=0.\end{aligned} \end{equation}$$

These are independent conservation laws. Adding USD and INR as though they were a single asset is dimensionally invalid. The economic value of the trade, liquidity sufficiency and commercial fairness of the rate are separate questions. The model must bind each account to the correct ledger, asset and scale and verify both liquidity constraints before claiming a successful atomic exchange.

13.1 Quote binding, rounding and retries

$$\begin{equation} \mathit{destination\_minor}=\operatorname{Round}_{\mathrm{mode}}\!\left(\mathit{source\_minor}\times\frac{\mathit{rate\_num}}{\mathit{rate\_den}}\times10^{\mathit{scale}_{\mathrm{destination}}-\mathit{scale}_{\mathrm{source}}}\right) \end{equation}$$

Represent a rate as an exact rational or a reviewed fixed-decimal value. For the example, 8242135/100000 is the rate; 10000 minor units produce 824213.5 destination minor units before rounding. A declared half-up rule yields 824214. This derivation demonstrates deterministic arithmetic for the example; it does not establish that the quoted market rate was correct.

The immutable quote receipt records assets and scales, rational rate, source/provider, timestamp, expiry, rounding mode, spread/fees, and a payload hash bound to the authorized operation. Prevent overflow in bounded production types even when the formal model uses unbounded naturals. Confirm that decimal scale changes invalidate dependent proofs and fixtures.

13.2 Fee and expiry semantics must be explicit

Record a fee/spread as an explicit additional transfer where applicable; the official recipe illustrates a separate fee leg in the linked chain. A business decision to incorporate a fee into a quote instead still needs an auditable decomposition. Do not hide accounting consequences inside a display rate. [33]

Define the expiry linearization point. “Quote valid when the backend accepted this operation” is different from “ledger commit must occur before expiry.” The latter needs an enforceable execution protocol and timing assumptions; a clock check before an RPC does not prove it. After timeout with unknown outcome, preserve the original authorized quote and transfer IDs while resolving that outcome. Never reprice an uncertain operation into new financial effects.

The formal law covers arithmetic and the modeled linked transition. Actual cluster atomicity, adapter encoding, price-provider authenticity and clock bounds remain separately identified premises or integration results.

For an illustrative E7 adapter, the example amounts become 1,000,000,000 USD ledger units and 82,421,400,000 INR ledger units, respectively. Both currency ledgers use E7 here; their minor-unit conversions remain separately checked. Conservation applies to each ledger’s debit/credit counters, not to a sum of USD and INR magnitudes.

14 Money example IV: corrections

TigerBeetle transfers are immutable. A mistake is corrected by new transfers that reverse or adjust the earlier effect; lineage belongs in explicit application/accounting metadata and identifiers. A posted transfer is not edited in place, and voiding an unresolved pending transfer is not the same operation as reversing a posted one. [28, 34]

$$\begin{equation} \begin{aligned}\operatorname{net}(\mathit{originals}+\mathit{corrections})&=\mathit{intended\_net},\\\mathit{originals}&\text{ remain immutable}.\end{aligned} \end{equation}$$

Define net as a vector indexed by ledger and account, in each asset’s own integer units. If the original posted effect is (+m at destination, $-$m at source), a full reversal appends the opposite vector. Their sum is zero, while the original record remains addressable. A partial correction appends only the authorized difference. The lineage must bind the original transfer, correction operation, amount, reason, approver and associated reconciliation amendment.

For a 10000-unit pending reservation posted for 6000, correction entitlement is based on the 6000 actually posted, not the original reservation. Returning 10000 would over-reverse. Concurrent corrections must atomically allocate the remaining entitlement in the modeled authority; distinct correction IDs alone do not prevent cumulative excess.

The abstract proof composes additive correction vectors and an immutable-history invariant. Backend integration must show that crashes between entitlement allocation and ledger acknowledgement cannot lose identity or permit another effect. If those steps cross stores, specify a recoverable protocol rather than assuming a distributed transaction that does not exist.

In counter vocabulary a reversal increments the new debit account’s $D^p$ and the new credit account’s $C^p$. It does not decrement the original posted counters. Net correction equality is an equality of derived signed positions plus immutable lineage, not an instruction to store a negative transfer amount.

15 UI observation protocols

The UI is an observation and command boundary, not an authorization authority. Let U be visible semantic state, L an island/reducer model, R a read projection and D the domain state. An honest interface may optimistically show Submitting or Pending; it must not claim Committed without versioned backend evidence for the same aggregate and operation.

$$\begin{equation} \begin{aligned}(U,L,R,D)&\rightarrow\mathit{request}\rightarrow\mathit{command}\rightarrow D^{\prime}\rightarrow R^{\prime}\\&\rightarrow\mathit{response/patch}\rightarrow(U^{\prime},L^{\prime},R^{\prime},D^{\prime})\end{aligned} \end{equation}$$

15.1 HTMX: request, target and swap

HTMX connects a user event to an HTTP request and an HTML-fragment update. The application declares the event, request method, target and swap behaviour. Request, response and swap lifecycle events are observable integration seams. An afterRequest or afterSwap event is not evidence that a financial operation committed. [35–37]

Model the chain explicitly: user event $\rightarrow$ HTTP request $\rightarrow$ authenticated server command $\rightarrow$ versioned fragment response $\rightarrow$ target selection $\rightarrow$ DOM swap $\rightarrow$ resulting visible state. The server must distinguish transport acceptance from durable domain completion. HTTP 202 does not mean that asynchronous processing completed successfully. [38]

Before applying an authoritative fragment, check aggregate ID, operation ID and version against the rendered region. A response from an older request must not overwrite a newer result. A Committed fragment requires an identified durable observation; a timeout fragment must not masquerade as a rejection if the effect may already exist.

Ownership and lifecycle

Give each live DOM region one owner. HTMX must not replace an Elm-owned root or a Datastar-owned region without an explicit mount/unmount protocol. Integration tests inspect target resolution, out-of-band updates, cancellation, browser reload, focus and island reinitialization. Proving a server transition does not prove that the browser swapped the intended fragment or preserved accessibility state.

15.2 Elm islands: a typed local core

The Elm Architecture separates Model, messages, Update and View. Ports bridge Elm to JavaScript and therefore form an explicit integration boundary. The Elm compiler’s type checks are useful, but they do not by themselves constitute a refinement proof for an application or prove that every external port value has the intended domain meaning. [39, 40]

Listing 7. Illustrative algebraic model, not compiled Elm or Bend code.

Model = Idle
      | Submitting(OperationId)
      | Pending(OperationId, Version)
      | Committed(OperationId, Version, Receipt)
      | Rejected(OperationId, Version, Reason)
      | Conflict(OperationId, LatestVersion)

Msg   = Submit | Retry | Cancel
      | Accepted(OperationId, Version)
      | DomainObserved(OperationId, Version, Status, Receipt)
      | TransportFailed(OperationId)

Local laws to prove in a formalized reducer

$$\begin{equation} \begin{aligned}\forall\text{ valid }(m,\mu):\quad&\operatorname{Update}(m,\mu)\text{ is defined},\\&\operatorname{version}(\operatorname{Update}(m,\mu))\geq\operatorname{version}(m),\\&\operatorname{View}(m)\text{ reflects the declared semantic state of }m.\end{aligned} \end{equation}$$

A total reducer handles every valid Model/Msg pair; an invalid external message is rejected by a typed decoder before it enters that domain. Algebraic variants prevent contradictory combinations such as a Committed state with no operation identity or receipt. A stale DomainObserved message is ignored or triggers a controlled resynchronization, never a regression. Tie every status to the correct operation; two operations on one aggregate must not share an ambiguous success banner.

A view theorem is relative to a normalized observation of the rendered view, not an arbitrary screenshot. A production connection can use verified reducer translation or language-specific verification; otherwise compare the actual Elm implementation with the model through property/state-machine tests. Ports must preserve IDs, versions, units and rejection semantics in both directions.

End-to-end check

PADST sends accepted, stale, duplicated, reordered and malformed port/domain messages around a payment submission. The simulation harness controls the relative timing of the domain event, projection advance and browser response. Browser integration verifies the real decoder, port wiring, region ownership and rendering lifecycle. UI state remains untrusted input when the backend decides whether a command may execute.

15.3 Datastar: versioned streams

Datastar supplies reactive signals and backend actions. Its SSE response protocol includes datastar-patch-elements and datastar-patch-signals; element patches normally morph ID-matched elements. These mechanisms do not themselves supply the application’s aggregate ordering, deduplication, authorization or durable-commit guarantees. [41–43]

Listing 8. Illustrative authoritative-patch envelope. The integration must define where this metadata is encoded and how it is checked before application.

# Proposed application metadata; not native Datastar fields.
aggregate_id: payment-42
operation_id: payment-42-submit-7
aggregate_version: 18
stream_id: payment-42-epoch-3
stream_sequence: 91
payload_hash: sha256:...
observation_receipt: sha256:...
patch_kind: datastar-patch-elements  # or patch-signals

$$\begin{equation} \begin{aligned}\operatorname{applied}(v_2)\text{ after }\operatorname{applied}(v_1)&\Rightarrow v_2\geq v_1,\\\operatorname{same}(\mathit{stream\_id},\mathit{sequence})&\Rightarrow\operatorname{same}(\mathit{payload\_hash}),\\\operatorname{Committed}(\mathit{version}=v)&\Rightarrow\exists\text{ durable domain observation at version }\geq v,\\\operatorname{reconnect}(\mathit{last\_event\_id})&\Rightarrow\text{rendered aggregate cannot regress}.\end{aligned} \end{equation}$$

Interpret these laws per aggregate and operation, not as one global version across the browser. Strengthen the commitment law to require a matching committed observation for that same identity and meaning; a newer unrelated event is not sufficient. Hash the canonical patch meaning, including target/mode where relevant, so a repeated sequence with a different payload is a protocol violation.

A stream restart needs an explicit epoch and cursor policy. Last-Event-ID is a transport cursor, not a domain version or an authorization token. Native EventSource semantics and Datastar’s Fetch-based backend-action transport are distinct; the selected client/adapter must define and test how reconnection state is carried. Reconnect alone does not establish application replay correctness. [42, 44]

Client-editable signals may express intent or optimistic state. They must never serve as evidence of permission, approval threshold, or durable commitment. The backend authenticates and authorizes every effect independently.

15.4 UI boundaries and adversarial delivery

An SSE failure trace

The browser renders aggregate version 18. The simulation harness delays its next projection update, delivers a duplicate patch (epoch 3, sequence 91), disconnects halfway through a new SSE event, then reconnects and offers a stale version-17 patch followed by version 19. PADST expects the duplicate to be harmless, incomplete framing to produce no partial authoritative update, version 17 to be rejected, and version 19 to apply only after valid identity and observation checks.

A sequence reused with a different payload hash is not another harmless duplicate: stop or resynchronize and record the conflict. If several element/signal patches together represent one authoritative state, define a versioned patch bundle and completion barrier. Do not expose a success label halfway through an incoherent bundle. These are proposed adapter semantics, not claims that Datastar supplies an atomic application transaction.

Visual layout, pixel correctness, focus, usability and assistive-technology behaviour remain browser/accessibility evidence. A semantic-state theorem cannot substitute for those checks.

16 Authorization and dual approval

Authentication establishes identity evidence; authorization decides whether that identity may perform a specific action. Model a payment with creator, canonical command hash, approvals, policy version, amount/risk band, status and an authorization epoch. OIDC token validation and Cedar policy evaluation are environmental/implementation boundaries, not consequences of a pure payment-state theorem. [45, 46]

$$\begin{equation} \begin{aligned}\operatorname{creator}(p)&\notin\operatorname{eligibleApprovers}(p,\mathit{policy\_version}),\\\operatorname{Executable}(p)&\Rightarrow|\operatorname{distinctEligibleApprovals}(p)|\geq\operatorname{required}(p),\\\mathit{approval.command\_hash}&=\mathit{payment.command\_hash}.\end{aligned} \end{equation}$$

For maker-checker with dual approval, require the specified number of distinct eligible identities, excluding the creator. Approval evidence is bound to the payment, action, command hash, policy version and validity interval. Execution re-evaluates current authorization according to an explicit policy for membership and policy changes. A stale approval cannot be silently grandfathered unless approved business policy explicitly permits that semantics.

The formal transition cannot construct Executable until the threshold and separation rules hold. Concurrent approvals require atomic deduplication or serialization in the implementation relation. Replayed or expired evidence must not increase the count. An ID token, a disabled button, or a client signal is not a backend payment permission.

Declare assumptions for issuer behaviour, key validity/rotation, token audience and replay controls, membership freshness, policy-store consistency, clock skew and availability. A proof assuming fresh identity data must not be reported as unconditional revocation enforcement.

17 Cross-repository GitHub Actions design

17.1 Component PR: untrusted candidate, trusted obligations

A component PR begins by resolving behavioural impact against protected baseline policy. The agent’s task file cannot choose the entire verification set. Reusable workflows are pinned to full commit SHAs, and proof tools, rules, observation functions and artifact-verification policy are independently controlled. GitHub documents SHA references as the safest reusable-workflow option. [47]

Untrusted PR code executes in isolated, disposable runners without signing or cross-repository credentials. A separate trusted verification/signing stage consumes validated immutable outputs and must not execute arbitrary candidate scripts with privileged tokens. A build job may produce malicious data; paths, archives, manifests and reports all need validation before a privileged consumer touches them. [48]

A reusable workflow pin does not by itself protect against executing attacker-controlled code in that workflow. Review its checkout target, tool installation, cache usage, permissions and artifact-handling boundary. The exact verifier workflow SHA becomes part of the evidence subject relation.

17.2 System verification and release

After merge

Publish an immutable component release, then open an automated system-manifest PR containing exact versions. Re-run composition and the affected evidence for that manifest; approve and deploy only its digest. Preserve the evidence alongside the deployment attestation. If a merge commit, merge queue result, build configuration or artifact differs from the tested candidate, rebind or rerun the affected checks rather than transferring a green badge by name.

A release controller verifies manifest approval, signature identity, artifact digests, policy version, result expiry and any required assumption freshness. A rollback is another explicit manifest selection: a previously tested old version may be incompatible with new schemas or infrastructure. Historical evidence is retained, but current deployment eligibility is evaluated anew.

Cross-repository completion is a protocol

A request ID correlates component PR, candidate manifest and verifier result. Deduplicate duplicate dispatches; ignore stale results for superseded PR heads; reject result substitution across repositories or manifests. The component repository must wait for the authenticated system verdict, not merely successful delivery of a dispatch request. [49, 50]

17.3 Credentials, triggers and attestations

Use OIDC federation with a narrowly scoped trust policy for artifact storage and signing. Validate issuer, audience, repository identity and workflow identity/ref as applicable; id-token permission is not authority to modify another GitHub repository. The normal GITHUB_TOKEN is scoped to its repository. Cross-repository dispatch and check reporting therefore require a separately authorized, short-lived credential—for example a narrowly installed GitHub App accessed through a trusted broker. [50–53]

Result binding: minimum signed fields

Listing 9. Illustrative result envelope; signing also binds the schema, assurance scope, assumptions and evidence locations.

original_repository_id: <stable-repository-id>
original_source_sha: <full-commit-sha>
candidate_manifest_hash: sha256:...
artifact_digests: [sha256:...]
contract_hashes: [sha256:...]
proof_hashes: [sha256:...]
padst_scenario_set: sha256:...
simulation_seed: <seed>
simulation_trace_digest: sha256:...
verifier_workflow_sha: <full-commit-sha>
result: <pass|fail|unknown>
expires_at: <timestamp>

GitHub artifact attestations and SLSA provenance provide relevant identity/subject machinery. The behavioural verdict is an additional governed assertion with its own verification policy, not an automatic interpretation of build provenance. [11, 12]

18 Governance of the judging criteria

AI agents and developers may write code and propose proofs. They must not silently weaken the laws, observations or assumptions against which their changes are judged. Protect Allium, generated-law sources, semantic IR definitions, translators, observation functions, policy and verifier workflows. Use CODEOWNERS and enforced review rules; where multiple approval domains are required, enforce each explicitly—listing several owners on one CODEOWNERS line does not require approval from all of them. [54]

Non-vacuity and mutation discipline

Every important law has feasible positive witnesses and mutations that should be rejected: remove an authorization guard, alter an asset scale, change rounding, hide an effect in the observation function, drop a proof obligation, regress a version comparator, or substitute a stale artifact. Mutations evaluate the gate’s ability to detect a defined defect; they do not prove the original implementation correct.

Compare the required obligation inventory with the baseline, including removed paths and dependencies. Explicitly list all axioms and unsafe operations; an approved exception remains an assumption with a named owner, affected scope and expiry. An implementation author cannot convert “unsupported” to “proven” by editing metadata. Preserve signed provenance and minimized failing traces with access control, retention policy and original witnesses.

Manual release is not proof. Where policy permits break-glass, record the exact degraded manifest, missing/failed obligations, human authority, reason, expiry and follow-up. Never relabel its assurance as passed or allow it to satisfy an automatic promotion gate.

19 Proven, tested, assumed and observed

Production monitors assumption drift

Telemetry should watch policy/config digests, key and identity-provider state, clock skew, queue redelivery, CDC lag and gaps, projection-version anomalies, reconciliation exceptions and actual deployment digests. An observed violation triggers the appropriate containment, re-verification or rollback process. Monitoring can detect breaches of E; a quiet dashboard cannot establish E for every unobserved instant or future execution.

Keep actual execution receipts separate from the architectural claims in this paper. A signed “pass” must state its formal subject, tested participants, scenario/fault bounds, and time of observation. Reviewers should be able to answer: which property, about which exact system, by which method, under which assumptions?

20 Software entropy and exergy: controlling uncertainty and preserving useful assurance

20.1 Origins, scope and corrections to the analogy

Physical exergy is useful work available relative to a specified reference environment; irreversible physical processes destroy it. Exergy analysis therefore depends on both system boundaries and environmental conditions. NASA’s systems-engineering treatment supplies a useful engineering reference, but does not establish a thermodynamic law of software correctness. Here, assurance exergy is a proposed policy metric: the useful assurance retained for an approved obligation inventory, reference manifest, observation map and fault model. Its units are policy points, not joules. A known-safe software state is a recovery target, not a thermodynamic dead state. Running a correct application does not imply equilibrium. [55]

The analogy motivates concrete questions: can an operation’s identity, authorization, debit/credit effects and corrective lineage still be reconstructed? Can a failed projection be rebuilt within a declared recovery envelope? It does not replace the five assurance classes, refinement obligations or independent approval of business intent. Allium records specifications; it does not prove them. Bend checks selected formal obligations. Testing examines implementations within its explored scope.

20.2 Entropy is uncertainty, not incorrectness

Shannon entropy requires a random variable and probability distribution, not merely a set of traces. If a justified distribution over a bounded random trace $T$ exists, $H(T\mid S,E)$ is conditional uncertainty given specification $S$ and evidence $E$. It is not generally computable for an arbitrary distributed implementation. Multiple permitted outcomes can retain positive entropy while every outcome is correct; a deterministic, certainly incorrect implementation can have zero entropy. Conditioning on approved intent does not make the implementation obey it. [56]

In particular, for an estimated violation probability $p$, binary entropy is $$\begin{equation} h_2(p)=-p\log_2p-(1-p)\log_2(1-p),\qquad h_2(0)=h_2(1)=0. \end{equation}$$ Minimizing this quantity can favor certainty of failure. It must not be a safety merge gate. Where calibrated probabilities exist, expected loss $\sum_o w_op_o$ is a different quantity; unknown probabilities remain unknown, rather than defaulting to zero. An assumed environment does not eliminate uncertainty about whether that environment will hold.

Similarly, $H(\Omega_{\mathrm{implementation}})-H(\Omega_{\mathrm{evidenced}})$ is undefined without compatible random variables, distributions and conditioning. This implementation does not publish that difference or assert that residual Shannon entropy approaches zero. Its enforceable objects are declared obligations, remaining evidence gaps, assumption inventories and mutation outcomes. New specified FX behavior can legitimately enlarge a state space; only a separately approved comparison policy can decide its required assurance.

Fotinós and Cabral’s 2026 preprint proposes a statistical-mechanics account of software entropy, with test constraints on implementation space and mutation analysis as a local approximation. That is a relevant emerging research direction, not a validated system-risk estimator or an established engineering standard. Mutation operators explore selected local syntactic changes, not all possible implementations or all production faults. [57]

20.3 Mutation adequacy with a protected denominator

Let $\mathcal{M}_o$ be the independently approved, executable mutant inventory for obligation $o$, with positive weights $v_m$. Let $K_o$ and $V_o$ denote killed and surviving mutants. Define a weighted survival ratio: $$\begin{equation} U_M(o)=\frac{\sum_{m\in V_o}v_m}{\sum_{m\in\mathcal{M}_o}v_m}. \end{equation}$$ This is an adequacy diagnostic, not Shannon entropy. Its denominator must be nonempty. A timeout, compiler error, infrastructure failure or unexecuted mutant is not a killed behavioral mutant. An equivalent mutant requires an independently reviewed exclusion and new inventory; a candidate cannot declare equivalence to improve its own score. Missing or additional inventory entries block the proposed comparison. Correlated and redundant mutants can inflate adequacy, so report operators, scope and excluded cases alongside the ratio. [58]

Financial operators should target stable transfer IDs, debit/credit direction, ledger and asset scale, pending resolution, linked-chain flags, authorization predicates, rounding, reconciliation matching and projection versions. Killing one ID-changing mutant does not eliminate every possible retry defect. A proof eliminates a modeled counterexample class only when the corresponding universal statement has actually been checked; testing an implementation mutant remains a separate result.

20.4 A policy score that cannot compensate away critical losses

Freeze a comparison frame $F$: reference manifest, candidate manifest, environmental assumptions, affected obligation closure, observation functions, scenario/mutant inventories, weights and score policy. For each obligation, retain consequence weight $w_o>0$, evidence credit $e_o\in[0,1]$ and scoped recovery credit $r_o\in[0,1]$. Then the proposed diagnostic is $$\begin{equation} X_A(F)=\sum_{o\in O_F}w_oe_or_o,\quad X_P(F)=\sum_{o\in O_F}w_o, \quad A(F)=X_P(F)-X_A(F). \end{equation}$$ Only when $X_P>0$ is $\eta_A=X_A/X_P$ defined. This is a policy-weighted coverage/quality score. It does not measure risk converted into certainty. Evidence classes are not interchangeable numbers: a bounded exhaustive model, sampled protocol test and production observation concern different subjects and assumptions. The earlier illustrative ranking from $1.00$ for connected proof to $0.15$ for review is not adopted as a universal ordering. Even a connected machine-checked proof retains specification and trusted-computing-base assumptions.

For an illustrative policy, the policy assigns a clearly illustrative ceiling of $700/1000$ to each semantic-simulation obligation. Earned evidence credit is that ceiling multiplied by $1-U_M$, rounded down to integer thousandths. Recovery credit is $1000$ only when every required scenario reports recovery, attributable trace and matching replay, otherwise zero. These conservative implementation rules make the score reproducible; they do not calibrate it scientifically. A score below potential can coexist with a policy pass and must remain visible as a shortfall.

Baseline and candidate must use the same approved frame. Define non-offsettable loss: $$\begin{equation} D_F=\sum_{o\in O_F}\max\{0,\,w_oe_o^{\mathrm{base}}r_o^{\mathrm{base}} -w_oe_o^{\mathrm{cand}}r_o^{\mathrm{cand}}\}. \end{equation}$$ For each protected obligation, require zero individual loss, all required critical mutants killed, and all required recovery observations satisfied. Also require $D_F\leq B_F$ across the declared closure. New obligations, retired behavior and changed weights require a reviewed baseline transition; an unrelated easy obligation cannot dilute a hard obligation or conceal its removal. Policy changes invalidate composition evidence.

The proposed identity “total potential = usable assurance + residual anergy + destroyed assurance” would double-count loss because $A=X_P-X_A$ already includes the candidate shortfall. No software conservation law follows from these definitions. Report $X_P$, $X_A$, $A$ and $D_F$ separately. Likewise, a final-state score cannot establish that a trace was safe at intermediate states.

20.5 Recoverability, safety and conditional progress

Existence of a recovery path is weaker than a strategy that works against the admitted environment. Let $I_{\mathrm{hard}}$ be protected safety, $Q$ a quiescent operational target, $\mathcal{F}$ the declared fault model, $\Pi(C)$ strategies over permitted corrective operations $C$. The intended obligations have the form $$\begin{equation} \forall\tau\in\mathrm{Traces}(M,E,\mathcal{F}):\quad \mathsf{G} I_{\mathrm{hard}}(\tau), \end{equation}$$ $$\begin{equation} \exists\pi\in\Pi(C)\;\forall\tau\in\mathrm{Traces}(M,\pi,E,\mathcal{F}):\quad \mathrm{Fair}_E(\tau)\Rightarrow\mathsf{G}(\mathrm{RecoveryNeeded}\Rightarrow\mathsf{F} Q). \end{equation}$$ Here $\mathsf{G}$ means always and $\mathsf{F}$ means eventually. A bounded deadline requires additional delivery, scheduling, availability and repair bounds. Repeated faults can prevent convergence indefinitely. A PADST run returning to $Q$ establishes one explored recovery trace, not this universal strategy property. Safety and liveness must remain separately stated. [59]

Legitimate financial commitment is often intentionally irreversible. The requirement is not that every payment can be undone: it is that identity, authorization, accounting history and any lawful correction or escalation remain attributable under declared constraints. Restoring an internal accounting position does not reverse an external settlement. An approved escalation preserves responsibility but does not itself restore money or resolve a pending ledger reservation.

20.6 Financial and UI examples

Transfer and pending counters. Model four nonnegative counters per account: $D_p,C_p,D_r,C_r$ for posted debits/credits and pending debits/credits. A same-ledger transfer of unsigned amount $a$ appends $a$ to the source’s posted debits and destination’s posted credits; it does not store a negative account balance. Pending creation increases the corresponding pending counters. Posting and voiding resolve the reservation according to TigerBeetle’s API; a partial post releases the remainder. Signed net observations are explicitly derived views. Per-ledger conservation constrains corresponding aggregate debit and credit movements, separately for posted and pending effects.

A response lost after commit must lead to lookup or retry with the same transfer identity. The protected observation includes operation ID, transfer ID, ledger, amount and account mapping. Creating a new ID on retry may conserve debits and credits while producing a second, unauthorized business effect: conservation alone is insufficient. No recovery score can excuse that violation.

TigerBeetle pending transfers can post, void or expire when configured with a timeout. Expiration disallows a later manual post or void; removal of expired pending balances is not guaranteed at the exact expiry instant. Thus a ledger liveness claim includes expiration and explicitly declared cluster/operational progress assumptions. A business escalation is recorded separately. The proposed drill should distinguish pending/void from timeout behaviour; a pending/void result alone does not certify a timeout service. [27]

FX. The USD and INR legs occupy different ledgers, using four accounts and a single linked chain. For the paper’s example, the source leg is 10,000 USD minor units and the destination leg 824,214 INR minor units. Each ledger conserves its own debits and credits; their numeric amounts must not be added as one conserved asset. In the rejection drill, insufficient INR liquidity must prevent both transfer creations. Removing linkage permits the USD leg to commit and is detected. Quote identity, asset scale, expiry, rounding and explicit fees remain separate obligations; linked atomicity does not establish commercial rate correctness. [33]

Corrections and reconciliation. Original transfers remain immutable. Corrective transfers append a lineage satisfying the intended net accounting effect under permitted limits. A recovery procedure must not silently replace the original operation or obscure a duplicate. Reconciliation closes only over immutable, hashed, bounded source cuts whose inventory is complete for the declared scope. Every item must be matched or assigned an accountable approved terminal exception, such as escalation. A difference classified as escalated is explained, not necessarily economically resolved; outstanding exposure, owner and deadline remain visible.

UI, identity and migration. A stale projection may recover by replay while the authoritative ledger never violates safety. An authoritative Datastar patch needs aggregate identity, operation identity, monotonic version and stream/sequence binding; matching sequence with conflicting payload must fail. An elevation banner or client signal is not authorization evidence. Recovery drills should include SSE reconnect, policy change during approval and interrupted migrations. Their absence is an explicit coverage gap, not something the three financial simulator drills can hide.

20.7 Artifacts, cross-repository gates and replication

A proposed recoverability policy pins a reference manifest, system evidence requirements, per-rule inventories, integer weights, baseline credits and a loss budget. The system receipt should bind a content-addressed report to the candidate manifest. Signature, freshness, build-provenance, assurance-class, execution-mode and participant checks still apply. Declared assumptions, traces, state snapshots and fault schedules must exist at their recorded hashes.

The verifier must recompute the score and hard gates rather than accepting a candidate’s precomputed total. Missing required evidence blocks admission. A changed policy invalidates the corresponding composition evidence. Protected reviewers approve baseline values and weights; a signature cannot make a false observation true.

A replication campaign should capture typed requests and all four ledger counters, inject response loss after commitment, run the declared recovery procedure, replay the same schedule and compare traces. It should also execute the corresponding mutants. Label simulated-adapter evidence separately from native-ledger integration and exact-artifact execution.

A finite admission model can check that admission requires the declared coverage and protection inputs. This does not prove a quantitative evaluator or financial adapter correct. Independently test missing reports, altered manifests, changed assumptions, unsafe trace prefixes, survivor substitution and score offsetting.

Publish an immutable input inventory, tool versions, permitted fixtures and a runnable driver before reporting campaign results. Keep failed runs and per-command outputs. A public reproduction command must not depend on inaccessible repositories, private pull requests or an unrecorded workstation layout. This edition describes that discipline without redistributing private operational evidence.

For a purely illustrative score, potential credit of 300 million units and earned credit of 210 million leave 90 million residual units. Such a number is policy accounting, not a measured probability of correctness; it cannot replace a critical invariant or missing recovery observation.

For scenario selection, consequence and irrecoverability can guide a reviewed priority order. A product $\Pr(\tau)\times\mathrm{Consequence}(\tau)\times\mathrm{Irrecoverability}(\tau)$ is an expected-loss heuristic only with justified probabilities and compatible scales. Fault injection frequency is not a production probability. Keep mandatory critical scenarios plus exploration outside the ranking so unknown or underestimated rare failures are not excluded.

20.8 Threats to validity and adoption limits

Weights, ceilings and baseline judgments are subjective and sensitive to decomposition. Splitting an obligation can inflate potential; reusing correlated evidence can double-count confidence. Freeze the semantic inventory, preserve the per-obligation vector and test sensitivity to policy choices. Noncritical scores must never override critical failures, unavailable evidence or undeclared environmental premises.

Mutation results depend on operator quality and scope. Replay depends on the controlled substrate, recorded inputs and implementation revision; a seed alone is insufficient. A successful simulator recovery cannot establish a production repair deadline, external bank truth, SaaS availability or pixel correctness. An explainability claim needs domain checks for causation and lineage, not merely nonempty logs. Loss of cryptographic keys, storage history or observation integrity can invalidate previously useful evidence.

The contribution is therefore an implementable assurance-quality and recoverability discipline, not a new proof calculus. Formal reasoning establishes the declared modeled properties; the proof graph composes scoped contracts; controlled protocol tests expose implementation divergence; governance prevents score and denominator manipulation. Entropy language is retained as a research motivation, while the actual gates use explicit obligations and non-offsettable losses.

21 Limitations and research evaluation

21.1 Threats to validity

Intent and translation. A correct proof of the wrong law remains wrong for the business. Allium’s behavioural authority depends on approval and precise selected semantics. The proposed translator, source maps and IR need their own correctness argument; deterministic output is insufficient.

Trusted computing base. The proof kernel, compiler/runtime, adapters, libraries, CI runner, artifact store, signing identity and deployment controller can invalidate the connection. Bend’s stated maturity limitations make independent qualification and narrow adoption important. Version pinning is necessary, not a proof of those dependencies. [9]

Abstraction and coverage. A simulated dependency may omit production behaviour; a “real node” wrapper may not execute the deployed path; an observation function can erase a violation. State explosion limits trace exploration. Finite controls and selected seeds cannot establish an unbounded universal claim.

Liveness and external truth. Availability depends on fairness, recovery and delivery assumptions. An external bank feed may be incomplete, a quote may be wrong, or an identity provider may be unavailable. Tests cannot remove these premises. Browser semantic correctness does not imply visual/usability correctness.

Evidence and governance. Signatures cannot repair a dishonest or compromised verifier. Incomplete impact graphs, stale caches, weak approval rules and untrusted workflow execution can create convincing but inapplicable evidence. Private source inspection is not independent experimental replication.

21.2 Public evaluation programme

Evaluate a narrow payment journey against a conventional CI baseline. Seed defects across numeric conversion, authorization, duplicate commands, linked-chain construction, CDC ordering, SSE regressions and reconciliation cuts. Record detection by formal checks, local tests, protocol scenarios, deterministic simulation and real integration separately. Retain undetected defects and false positives rather than collapsing them into one pass rate.

Measure obligation and real-adapter coverage, mutation survival, reproducibility of failing traces, reduction effectiveness, proof maintenance effort, verification latency, graph-invalidation precision and operational escapes. Repeat at fixed manifest versions and compare samples with comparable fault budgets. Publish the corpus, search bounds and exclusions where confidentiality permits. This paper supplies the architecture and evaluation design; it does not invent performance or correctness measurements for a completed deployment.

The included arithmetic example is a deliberately narrow formal core. Its local check report identifies the supplied laws, example execution and negative control exercised for this edition. It does not establish full-language translation, cross-repository release certification, production connectivity or native ledger integration.

Native integration studies should pin a disposable server and client, record source and executable identities, and test both sides of a historical cutoff. Keep these observations separate from simulation, durability and failover claims. Publish runnable artifacts and actual results before claiming execution.

22 Adoption and conclusion

22.1 A layered assurance system

The complete approach is not “formal proof versus testing.” Allium records approved intent. Bend proves mathematical properties of the formal core. Cross-repository assume-guarantee reasoning composes component contracts. PADST exercises real implementations using protocol-aware stateful traces, while the simulation harness makes the supported distributed execution deterministic, fault-controlled and replayable.

Integration tests validate external boundaries. Production telemetry checks whether environmental assumptions continue to hold where they can be observed; it cannot establish them universally. Governance prevents agents or developers from weakening invariants, preconditions, observations, assumptions, authorization, reconciliation completeness, asset scales, rounding, FX rate binding or deployment constraints merely to make CI pass.

Strongest defensible system claim. For the exact component versions and artifacts named in the approved system manifest, the formal core satisfies the declared laws; affected repository contracts compose under the stated assumptions; and the deployed implementations have passed protocol-aware adversarial traces in a deterministic execution environment.

That claim is earned only when the required implementation connections and execution capabilities are established for the named manifest. The proposed architecture is a route toward it, not evidence that the reference platform already satisfies it. It must not be shortened to “the whole platform is mathematically proven.”

Appendix: Complete runnable model and proofs

These are the same source files consumed by make research-examples; they are included directly into this document rather than maintained as separate listings. The natural-number model is deliberately small. The fixture amounts are bounded examples, while the checked laws quantify over all states represented by the model under the checker assumptions.

Listing 10. Balance.bend: total reservation function and its conservation proposition.

import Base

type Decision is Data:
  Accepted{remaining: Nat}
  Rejected{}

def reserve(request: Nat, remaining: Nat) -> Decision:
  match request:
    case 0n:
      Accepted{remaining}
    case 1n+r:
      match remaining:
        case 0n:
          Rejected{}
        case 1n+b:
          reserve(r, b)

def Conserves(outcome: Decision, -request: Nat, -remaining: Nat) -> Type:
  match outcome:
    case Accepted{left}:
      {Nat.add(request, left) == remaining : Nat}
    case Rejected{}:
      Unit

Listing 11. Payment.bend: the executable single-operation transition function and total-balance observation.

import Base
import ./Balance.bend as Balance

type Payment is Data:
  Pending{source: Nat, destination: Nat}
  Committed{source: Nat, destination: Nat}
  Rejected{source: Nat, destination: Nat}

def finish(outcome: Balance.Decision, amount: Nat,
           source: Nat, destination: Nat) -> Payment:
  match outcome:
    case Balance.Accepted{left}:
      Committed{left, Nat.add(amount, destination)}
    case Balance.Rejected{}:
      Rejected{source, destination}

def apply(+amount: Nat, state: Payment) -> Payment:
  match state:
    case Pending{+source, +destination}:
      finish(Balance.reserve(amount, source), amount, source, destination)
    case Committed{source, destination}:
      Committed{source, destination}
    case Rejected{source, destination}:
      Rejected{source, destination}

def total(state: Payment) -> Nat:
  match state:
    case Pending{source, destination}:
      Nat.add(source, destination)
    case Committed{source, destination}:
      Nat.add(source, destination)
    case Rejected{source, destination}:
      Nat.add(source, destination)

type RetryReply is Data:
  Refused{state: Payment}
  Replayed{state: Payment}

def retry(state: Payment) -> RetryReply:
  match state:
    case Pending{source, destination}:
      Refused{Pending{source, destination}}
    case Committed{source, destination}:
      Replayed{Committed{source, destination}}
    case Rejected{source, destination}:
      Replayed{Rejected{source, destination}}

def retry_state(reply: RetryReply) -> Payment:
  match reply:
    case Refused{state}:
      state
    case Replayed{state}:
      state

def retry_accepted(reply: RetryReply) -> Bool:
  match reply:
    case Refused{state}:
      False{}
    case Replayed{state}:
      True{}

def terminal(state: Payment) -> Bool:
  match state:
    case Pending{source, destination}:
      False{}
    case Committed{source, destination}:
      True{}
    case Rejected{source, destination}:
      True{}

type Observation is Data:
  Snapshot{source: Nat, destination: Nat, committed_effects: Nat}

def observe(state: Payment) -> Observation:
  match state:
    case Pending{source, destination}:
      Snapshot{source, destination, 0n}
    case Committed{source, destination}:
      Snapshot{source, destination, 1n}
    case Rejected{source, destination}:
      Snapshot{source, destination, 0n}

Listing 12. PROOF.bend: complete proof terms for the six laws, including the supporting arithmetic lemmas. Checked by Bend 2.0.16.

import Base
import ./Balance.bend as Balance
import ./Payment.bend as Payment
import ./LAWS.bend as Laws

def lift(outcome: Balance.Decision, -amount: Nat, -source: Nat,
         proof: Balance.Conserves(outcome, amount, source)) ->
         Balance.Conserves(outcome, 1n+amount, 1n+source):
  match outcome:
    case Balance.Accepted{left}:
      %proof : {1n+Nat.add(amount, left) == 1n+_ : Nat}
      {==}
    case Balance.Rejected{}:
      Unit{}

def Laws.reservation_conserves(amount, source):
  match amount:
    case 0n:
      {==}
    case 1n+ +rest:
      match source:
        case 0n:
          Unit{}
        case 1n+ +remaining:
          lift(Balance.reserve(rest, remaining), rest, remaining,
               Laws.reservation_conserves(rest, remaining))

def finish_idempotent(outcome: Balance.Decision, amount: Nat,
                      source: Nat, destination: Nat) ->
  {Payment.apply(amount, Payment.finish(outcome, amount, source, destination)) ==
   Payment.finish(outcome, amount, source, destination) : Payment.Payment}:
  match outcome:
    case Balance.Accepted{left}:
      {==}
    case Balance.Rejected{}:
      {==}

def Laws.duplicate_submit_idempotent(amount, state):
  match state:
    case Payment.Pending{+source, destination}:
      finish_idempotent(Balance.reserve(amount, source), amount, source, destination)
    case Payment.Committed{source, destination}:
      {==}
    case Payment.Rejected{source, destination}:
      {==}

def add_successor(a: Nat, +b: Nat) ->
  {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+ +p:
      %add_successor(p, b) : {1n+1n+Nat.add(p, b) == 1n+_ : Nat}
      {==}

def reassociate(a: Nat, +b: Nat, +c: Nat) ->
  {Nat.add(a, Nat.add(b, c)) == Nat.add(Nat.add(a, b), c) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+ +p:
      %reassociate(p, b, c) :
        {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
      {==}

def swap_add(a: Nat, +b: Nat, +c: Nat) ->
  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}:
  match a:
    case 0n:
      {==}
    case 1n+ +p:
      %add_successor(b, Nat.add(p, c)) :
        {1n+Nat.add(p, Nat.add(b, c)) == _ : Nat}
      %swap_add(p, b, c) :
        {1n+Nat.add(p, Nat.add(b, c)) == 1n+_ : Nat}
      {==}

def finish_conserves(outcome: Balance.Decision, +amount: Nat,
                     source: Nat, +destination: Nat,
                     proof: Balance.Conserves(outcome, amount, source)) ->
  {Payment.total(Payment.finish(outcome, amount, source, destination)) ==
   Nat.add(source, destination) : Nat}:
  match outcome:
    case Balance.Accepted{+left}:
      %proof : {Nat.add(left, Nat.add(amount, destination)) ==
                Nat.add(_, destination) : Nat}
      %reassociate(amount, left, destination) :
        {Nat.add(left, Nat.add(amount, destination)) == _ : Nat}
      swap_add(left, amount, destination)
    case Balance.Rejected{}:
      {==}

def Laws.transfer_conserves(amount, state):
  match state:
    case Payment.Pending{+source, +destination}:
      finish_conserves(Balance.reserve(amount, source), amount,
                       source, destination,
                       Laws.reservation_conserves(amount, source))
    case Payment.Committed{source, destination}:
      {==}
    case Payment.Rejected{source, destination}:
      {==}

def Laws.retry_preserves_state(state):
  match state:
    case Payment.Pending{source, destination}:
      {==}
    case Payment.Committed{source, destination}:
      {==}
    case Payment.Rejected{source, destination}:
      {==}

def Laws.retry_requires_terminal(state):
  match state:
    case Payment.Pending{source, destination}:
      {==}
    case Payment.Committed{source, destination}:
      {==}
    case Payment.Rejected{source, destination}:
      {==}

def Laws.observed_retry_stable(state):
  %Laws.retry_preserves_state(state) :
    {Payment.observe(Payment.retry_state(Payment.retry(state))) ==
     Payment.observe(_) : Payment.Observation}
  {==}

Listing 13. cases.json: concrete input data and expected states used by the executable fixture checks. Every amount is an integer number of USD cents.

{
  "asset": "USD",
  "scale": 2,
  "scope": "Concrete test fixtures for a single operation; not production transactions",
  "cases": [
    {
      "id": "first_submit",
      "operation_id": "demo-usd-001",
      "source": 125,
      "destination": 25,
      "expected": {
        "status": "Committed",
        "source": 25,
        "destination": 125
      },
      "amount": 100,
      "events": [
        {
          "kind": "submit"
        }
      ]
    },
    {
      "id": "retry_after_commit",
      "operation_id": "demo-usd-001",
      "source": 125,
      "destination": 25,
      "expected": {
        "status": "Committed",
        "source": 25,
        "destination": 125
      },
      "amount": 100,
      "events": [
        {
          "kind": "submit"
        },
        {
          "kind": "retry"
        }
      ]
    },
    {
      "id": "insufficient_funds",
      "operation_id": "demo-usd-002",
      "source": 125,
      "destination": 25,
      "expected": {
        "status": "Rejected",
        "source": 125,
        "destination": 25
      },
      "amount": 200,
      "events": [
        {
          "kind": "submit"
        }
      ]
    },
    {
      "id": "retry_after_rejection",
      "operation_id": "demo-usd-002",
      "source": 125,
      "destination": 25,
      "expected": {
        "status": "Rejected",
        "source": 125,
        "destination": 25
      },
      "amount": 200,
      "events": [
        {
          "kind": "submit"
        },
        {
          "kind": "retry"
        }
      ]
    },
    {
      "id": "retry_before_submit",
      "operation_id": "demo-usd-003",
      "source": 125,
      "destination": 25,
      "amount": 100,
      "events": [
        {
          "kind": "retry"
        }
      ],
      "expected": {
        "status": "Pending",
        "source": 125,
        "destination": 25
      }
    },
    {
      "id": "duplicate_submit_model",
      "operation_id": "demo-usd-004",
      "source": 125,
      "destination": 25,
      "amount": 100,
      "events": [
        {
          "kind": "reduce_submit"
        },
        {
          "kind": "reduce_submit"
        }
      ],
      "expected": {
        "status": "Committed",
        "source": 25,
        "destination": 125
      },
      "scope": "algebraic reducer property; not credited as RetryPayment"
    }
  ]
}

References