verified eventual consistency: formalization

definition

Verified Eventual Consistency (VEC) is a consistency model for distributed systems where correctness is VERIFIABLE locally, not ASSUMED globally. it extends eventual consistency with three cryptographic guarantees.

a distributed system satisfies VEC if six properties hold:

P1: safety (convergence)

for any two correct nodes A and B with signal sets $S_A$ and $S_B$:

$$S_A = S_B \implies \text{state}(S_A) = \text{state}(S_B)$$

this follows from CRDT properties. the merge function is a join-semilattice: commutative ($a \sqcup b = b \sqcup a$), associative ($(a \sqcup b) \sqcup c = a \sqcup (b \sqcup c)$), idempotent ($a \sqcup a = a$). equal sets under a deterministic lattice merge produce equal states.

the algorithm is G-Set union for independent signals, topological sort by (causal order, VDF time, hash tiebreak) for dependent signals:

merge(S):
  sorted ← topological_sort(S, order = causal > vdf > hash)
  state ← initial_state
  for signal in sorted:
    state ← apply(state, signal)
  return state

deterministic: same set produces same sort produces same sequence produces same state.

P2: completeness (verifiable set equality)

a node can verify in O(log n) whether its signal set for a given source is complete:

$$\text{verify\_complete}(S_A^{(\nu)}, \text{steps}[a, b]) \to \{\text{true}, \text{false}\}$$

algorithm: NMT completeness proof. each source (device or neuron) commits its signal chain to a per-source NMT namespaced by step counter:

NMT_ν[step → H(signal)]

completeness_proof(ν, range [a,b]):
  path_left  ← merkle_path(leftmost leaf with step ≥ a)
  path_right ← merkle_path(rightmost leaf with step ≤ b)
  boundary_left  ← neighbor with step < a (or tree boundary)
  boundary_right ← neighbor with step > b (or tree boundary)
  return (paths, boundaries, leaves)

verify_complete(proof, root, range [a,b]):
  check path_left valid against root
  check path_right valid against root
  check boundary_left.step < a
  check boundary_right.step > b
  check sorting invariant: all leaves sorted by step
  → structurally impossible to omit a leaf in [a,b]

cost: O(log n) Hemera hashes for proof, O(log n) for verification. the guarantee is unconditional -- it depends only on collision resistance of Hemera, not on honest majorities or protocol execution.

P3: availability (verifiable data existence)

a node can verify in O(sqrt(n)) whether the data underlying its signal set physically exists across the network:

$$\text{verify\_available}(\text{root}, k) \to \{\text{available}, \text{unavailable}\}$$

algorithm: DAS with 2D Reed-Solomon erasure coding over Goldilocks field:

encode(data, rate=1/2):
  grid ← reshape(data, √n × √n)
  for each row:  extended_row ← reed_solomon_encode(row, rate)
  for each col:  extended_col ← reed_solomon_encode(col, rate)
  return extended_grid  # 2√n × 2√n

commit(extended_grid):
  for each row: row_root ← NMT(row cells, namespace = position)
  col_root ← NMT(row_roots)
  return col_root

sample(root, k=20):
  for i in 1..k:
    pos ← random_position()
    (cell, proof) ← request(pos)
    if not verify_nmt_proof(cell, proof, root): return unavailable
  return available  # confidence ≥ 1 - (1/2)^k

# k=20: 99.9999% confidence
# k=30: 99.99999999% confidence

the guarantee is probabilistic but information-theoretic -- it depends on sampling randomness, not computational hardness. with rate 1/2 encoding, withholding >50% of data makes reconstruction fail, but random sampling detects it with probability approaching 1 exponentially in k.

P4: liveness (eventual delivery)

if a signal is created by a correct node and the network is eventually connected, every correct node eventually receives it:

$$\forall s \in \text{created\_signals}, \exists t: \forall \text{correct } A, s \in S_A^{(t)}$$

this relies on gossip protocol + erasure coding reconstruction. if some chunks are lost, any k-of-n surviving chunks reconstruct the original. the liveness bound depends on network connectivity and gossip propagation -- same as standard eventual consistency, but strengthened by erasure reconstruction.

P5: validity (provable state transitions)

every signal carries a zheng proof sigma covering all operations in the batch:

$$\text{verify\_signal}(s, \sigma) \to \{\text{valid}, \text{invalid}\}$$

algorithm: SuperSpartan IOP + Brakedown PCS over Goldilocks field:

verify_signal(signal, proof):
  1. init transcript T from signal commitment
  2. for i in 1..k (sumcheck rounds):
     gᵢ ← proof.round_polynomials[i]
     assert gᵢ(0) + gᵢ(1) = previous_claim
     T.absorb(gᵢ)
     rᵢ ← T.squeeze()  # Fiat-Shamir via Hemera
  3. assert final_claim = constraint_eval(proof.value, r, statement)
  4. assert Brakedown_verify(commitment, r, proof.value, proof.opening)

cost: O(log N) Hemera hashes + field ops. ~50 us independent of computation size (recursive proof compresses all history). an invalid signal cannot be constructed -- the constraint system (18 patterns of nox: 16 compute + call + look) prevents it.

P6: ordering (immutable causal structure)

every signal carries embedded ordering metadata:

signal.prev         = H(author's previous signal)     # hash chain
signal.merkle_clock = H(all known signal hashes)       # compact causal state
signal.vdf_proof    = VDF(prev, T_min)                 # physical time
signal.step         = monotonic counter                 # logical clock

properties:

• hash chain: immutable per-source history. inserting/removing/reordering signals breaks chain hashes. detectable by any peer in O(1) -- compare prev fields
• VDF: physical rate limit. each signal costs T_min sequential wall-clock computation. equivocation (two signals with same prev) costs 2xT_min -- detectable because total VDF time exceeds elapsed wall time
• deterministic total order from data alone: causal > VDF time > hash tiebreak. no coordination needed

the full model: VEC+ = P1 + P2 + P3 + P4 + P5 + P6

each property has a different guarantee type. each comes from a different branch of mathematics. each is independently verifiable. this is compositional security -- failure of one layer does not compromise others.

minimality conjecture

conjecture: P1 + P2 + P3 is the minimum for verified convergence without coordination.

argument by elimination

• remove P1 (convergence): equal sets produce different states. verification of completeness and availability is useless if the merge is non-deterministic
• remove P2 (completeness): convergence on incomplete data produces wrong state. availability proves data exists but not that you have all of it
• remove P3 (availability): convergence on complete data that no longer exists. NMT proves you had everything, but the data may be lost

each removal loses a property the other two cannot provide. the three core properties are orthogonal.

algebraic NMT optimization

the algebraic-nmt proposal replaces NMT trees with polynomial commitments:

current (NMT + CRDT):
  completeness: NMT sorting invariant (structural)
  merge: G-Set union (algebraic)
  → two independent structures

algebraic NMT:
  completeness: polynomial evaluation proof (algebraic)
  merge: polynomial addition (algebraic)
  → one structure providing both

cost reduction:
  current: ~106K constraints per cyberlink (NMT paths)
  algebraic: ~3.2K constraints (PCS evaluation)
  → 33× improvement

if completeness and merge share a single polynomial commitment scheme, the minimum composition reduces from algebra + logic + probability to algebra + probability. two layers instead of three. the lower bound conjecture would need revision.

vertical composability (the stack)

the cyber proof stack composes vertically:

application (cybergraph operations)
     ↓ expressed as
nox (18 patterns: 16 compute + call + look, focus-metered execution)
     ↓ proven by
zheng (SuperSpartan IOP + Brakedown PCS)
     ↓ committed via
hemera (Poseidon2 hashing, NMT/MMR construction)
     ↓ over
nebu (Goldilocks field arithmetic, p = 2⁶⁴ - 2³² + 1)

each layer provides guarantees consumed by the layer above:

• nebu: field operations are correct (algebraic closure)
• hemera: hashes are collision-resistant (2^128 security, margin 2^918)
• zheng: proofs are sound (sumcheck + Brakedown, error <= 2^-512 at k=16)
• nox: execution is focus-metered (halt guaranteed)
• application: state transitions are valid

horizontal composability (cross-graph)

if system A uses VEC and system B uses VEC, does A x B inherit VEC?

P1 (convergence): yes, if the merge functions are independent. CRDT products are CRDTs -- the product lattice of two join-semilattices is a join-semilattice

P2 (completeness): yes, if namespaces are disjoint. NMT proofs for namespace A and namespace B are independent. the NMT structure naturally supports this -- each system occupies a namespace range

P3 (availability): yes, if erasure coding is independent. DAS samples for A and B are separate. availability of A does not depend on availability of B

P4-P6: inherit straightforwardly from per-signal properties

cross-graph cyberlinks (A links to B) require: NMT inclusion proof in both namespaces. this is O(log n_A + log n_B) -- additive, not multiplicative

optimization directions

the complete optimization path: nebu provides fast field ops, hemera uses them for efficient hashing, zheng uses hemera for transparent proofs, nox uses zheng for provable execution, bbg uses everything for authenticated state. top-down: application demands drive optimization targets. bottom-up: field arithmetic improvements cascade through every layer.

this bidirectional optimization is why the stack exists as separate repos -- each layer can be improved independently while the interfaces remain stable. a 2x improvement in Hemera permutation speed cascades to 2x faster NMT updates, 2x faster proof generation, 2x faster state transitions. a 33x reduction in NMT constraints (algebraic NMT) cascades to 33x cheaper cyberlinks, 33x more throughput, 33x lower per-signal cost.

see structural sync for the five-layer theory. see cyb/fs/sync for the unified patch+sync specification. see bostrom-to-onnx-pipeline for how graph structure compiles into transformer parameters. see algebraic-nmt for the polynomial NMT proposal. see spectral gap from convergence for the empirical observation that convergence is faster than predicted