Monthly research note. Theme: Blockchain Protocols.

TL;DR

Formalizing a Blockchain Protocol: Properties Worth Proving as an engineering constraint: write down assumptions, make invariants executable, and design operational recovery as part of correctness.

Key insight

Most failures are boundary failures: parsing, persistence, concurrency, retries, and upgrades.

Key takeaways

  • Consensus safety is meaningless if execution is nondeterministic across nodes.
  • Finality guarantees are user security guarantees—document and enforce them.
  • Mempools are adversarial schedulers: admission and fairness are protocol concerns.
  • Define safety properties before performance goals.
  • Prefer protocols and APIs that make invalid states hard to express.

Why this matters

  • Light clients shift assumptions; they must be written down.
  • MEV turns protocol details into adversarial strategy.
  • Topology attacks (eclipse, partition) change who sees which transactions.
  • Finality guarantees are user security guarantees; ambiguity is a UX vulnerability.

Key questions

  • How do upgrades change security assumptions (fork choice, state transition rules)?
  • How do you defend against topology attacks (eclipse, partition, sybil)?
  • What is the reorg budget for applications and how do you communicate it?
  • What is the finality guarantee users can rely on (and when does it break)?
  • Where is the economic/DoS pressure applied (mempool, gossip, execution, storage)?
  • Where do you enforce resource limits (gas, bandwidth, storage, signature checks)?

Assumptions

  • Upgrades happen under partial adoption; mixed-version is inevitable.
  • Users and apps rely on probabilistic finality until proven otherwise.
  • Peers are untrusted; gossip can be manipulated for delay or isolation.
  • Nodes are heterogeneous; determinism must survive platform differences.

Non-goals

  • Relying on client-side heuristics to paper over protocol ambiguity.
  • Allowing execution nondeterminism for performance convenience.
Attack surface

Negotiation and fallbacks are where security silently becomes optional—treat them as hostile.

Model & invariants

A simple resource-admission constraint:

∑tx∈Bcost(tx)≤budget(B)(gas/bytes/sigchecks).\sum_{tx \in B} \mathrm{cost}(tx) \le \mathrm{budget}(B)\qquad\text{(gas/bytes/sigchecks)}.

Model the mempool as an adversarial scheduler: it chooses which work gets executed.

Treat reorgs as a user-visible security event; encode reorg-aware semantics.

Invariant

Invariants must be checkable from evidence you actually have (state + logs + counters).

Security properties

  • Downgrade resistance: negotiation can’t silently weaken security posture.
  • Least authority: privileges are scoped by purpose and time.
  • Evidence: critical actions emit verifiable audit events.
  • Replay resistance: duplicated inputs do not change outcomes.

Failure modes

  • Recovery paths that only work when nothing is broken.
  • Resource exhaustion (CPU/bandwidth/storage) turning into correctness failures.
  • Observability gaps during incidents (missing evidence).
  • Mixed-version behavior that violates assumptions silently.
Pitfall

Mixed-version deployments create states you never tested—plan for them explicitly.

Design sketch

sequenceDiagram
  participant U as User
  participant N as Node
  participant P as Peers
  U->>N: submit(tx)
  N->>P: gossip(tx)
  P-->>N: gossip(more tx)
  Note over N: admission + ordering
  N-->>U: inclusion/finality signal

Implementation notes

Treat mempool policy as part of the protocol if it changes security outcomes.

Rule of thumb

Acknowledge only after durability (or make “ack” explicitly best-effort).

Mempool hardening checklist:
- Per-peer rate limits + global admission budget
- Duplicate detection and eviction policy
- Signature verification batching with caps
- Anti-DoS: bounded decode/parse cost
- Fairness: per-sender quotas (avoid hot-account starvation)

Verification strategy

  • Formal invariants for supply/balance conservation where appropriate.
  • Fork/reorg simulations: application-facing invariants under reorgs.
  • Cross-implementation tests when multiple clients exist.
  • Adversarial mempool tests: spam, pinning, worst-case signature patterns.
  • Determinism tests across architectures (x86/ARM) and OSes.

Operational notes

  • Rehearse upgrades with mixed versions and rollback paths.
  • Measure invalid tx rejection reasons and rates (spam signature).
  • Protect peer tables against eclipse attempts (diversity, scoring, rotation).
  • Monitor reorg depth and frequency; treat increases as incidents.
  • Keep execution resource limits explicit and enforced.
Operational note

Attach explicit rollout/rollback triggers to changes that touch security or correctness.

What to monitor

  • Admission-control / rate-limit rejections (by reason).
  • Rollback events and the conditions that triggered them.
  • Retry/timeout rates by endpoint and client cohort.
  • Authz failures and policy denials (unexpected spikes).
  • Error budget burn + tail latency under load.

Rollback plan

  • Keep dual-write / dual-verify windows where appropriate.
  • Use canaries and staged rollout; stop early when signals degrade.
  • Define an explicit rollback trigger (metrics + thresholds).
  • Prefer backward-compatible changes; avoid “flag day” upgrades.
  • Preserve evidence (configs, artifacts, audit logs) to reconstruct what changed.

Evidence

  • Site Reliability Engineering (Google) (1) — Error budgets, incident response, and reliability as an engineering discipline.
    • Evidence: Error budgets and incident response are correctness controls; tie monitoring and rollback triggers to SLO burn.
  • Learn TLA+ (2) — Practical entry point for specification and model checking.
    • Evidence: Model the smallest thing that can break; use model checking to validate invariants before optimizing.

Open questions

  • What is the worst-case work a single transaction can force?
  • Which invariants should be proven vs tested vs monitored?
  • Where does your implementation accidentally depend on local wall-clock time?
  • How do you communicate finality uncertainty to users without lying?

Checklist

  • Rollback plan rehearsed and automated.
  • Failure modes enumerated with mitigations.
  • Assumptions listed and reviewed.
  • Safety properties stated as invariants.
  • Telemetry captures correctness signals.
  • Costs bounded (CPU/memory/bandwidth) under adversarial inputs.

Further reading

1.
Beyer B, Jones C, Petoff J, Murphy NR. Site Reliability Engineering: How Google Runs Production Systems [Internet]. O’Reilly Media; 2016. Available from: https://sre.google/sre-book/table-of-contents/
2.
LearnTLA. Learn TLA+ [Internet]. Web; Available from: https://learntla.com/