DECISIONS, EXPLAINED
Paxos Odin Discussions
Design records, protocol contracts and dated verification evidence. Each record states its status; an open proposal is not an implemented feature.
The Paxos Odin Discussion Process
Defines the POD lifecycle, numbering workflow, Typst project layout, registry, and CLI automation for the paxos-odin project.
Download PDFPaxos-Odin: Architecture and Pure State Machine Design
Specifies the 0.2.0 core: a deterministic effect machine over a data-oriented Ledger whose columns are Lamport's variables, bitmaps and bit_set_next scans, packed ballots, pointer payloads, the exact Effects capacities, the ten core files, canonical membership lookup, the replicated log, the learner, the error contract, and the verification that exists today.
Download PDFDurability Contracts, Window Reuse, and Trim Anchors
Formalizes the persist-then-send rule, the five durable records and their pointer payloads with the journal-copy obligation, the durability gates, the pre-durable rule and its round-zero exception, the memory floor and window reuse rules on the Ledger, hashless trim anchors, and the ledger_apply versus ledger_replay_fold replay contract.
Download PDFFast-Path Leader Leases and Linearizable Read Verification
Unimplemented lease proposal: identifies the clock, quorum, restart and applied-prefix proof obligations; logical ticks and caught-up queries provide no lease authority.
Download PDFThe Idiomatic Odin API Surface
Records the 0.1.0 and 0.2.0 API decisions: Ada_Case names, receiver-prefixed spellings plus proc-group verbs, Node_Options with rotating_ownership, Effects mirroring Node, Node_Id as u16, the packed Ballot, the Ledger and its proc group, pointer payloads and the Packet idiom, two before-and-after tables, and the rejected alternatives.
Download PDFReconfiguration and Epoch Isolation
Specifies stop signs on one slot line over the Ledger, Log_Sealed from pending through decided, pending_stop_sign for crash repair, init_from_stop and continue_at, strictly increasing configuration ids, Log_Envelope and the checked step, how stop signs behave under rotating ownership, the seeded handover scenarios, and the open questions.
Download PDFReview Findings and Verification Evidence
Preserves the five-pass 2026-09-16 review and the 2026-09-17 recovery follow-up: the correctness findings and repairs, Odin design choices, the error contract, verification evidence, host limits, the recorded 0.1.0 benchmark figures, the parity table with paxos-zig 0.7.0, the API and protocol changes, and the third pass: the data-oriented redesign, the ownership safety bug the simulator caught, and the 0.2.0 verification counts.
Download PDFSafety Argument: Axioms, Lemmas, and Proof Obligations
States the safety argument for the 0.2.0 core as axioms assumed of the host, lemmas about ballots, quorums, and votes, and proof obligations that name the procedures discharging them.
Download PDFThe Data-Oriented Ledger
Records the 0.2.0 layout: the per-message copying problem, Lamport's variables as columns with bitmaps and slot tags, the pointer contract, memory formulas per configuration, what the benchmark measures, the power-of-two and u16 constraints, and the rejected alternatives.
Download PDFRotating Slot Ownership
Specifies rotating slot ownership: round-robin slot ownership, the round-zero ballot reserved for each owner, no-op skips, bounded revocations with per-decree promises, and resubmission of revoked suggestions.
Download PDFPaxodin: A Python SDK over the Odin Core
A uv-managed Python 3.12+ package over a retained-batch C ABI: typed Session and Node APIs, durable journal and history, a validating wire codec, platform wheels built from an sdist outside the checkout, and four-path measured evidence. Reconfiguration, ownership, learners and leases are refused by capability bit.
Download PDF