Proofs

From a Separate Entry to a Functor Tower: Folding the Composition into Cross-Domain State Preservation

A design-correction note from the Oraclizer verification track. We fold a separate Isabelle/HOL entry into revision 3 of the existing one, where three category-axiom theorems make the Cross-Domain State Preservation Functor a proved object. The sync degree hierarchy is then formalized as a tower of functors joined by natural transformations.

Oraclizer Core ⋅ Jun 02, 2026

Designing Compositional State Assurance: Three Locales and One Glue

A month after the prelude, the compositional verification design is locked. Three decisions: glue predicate as state_join and state_refines, fair_leader positioned within the Heard-Of Model deterministic abstraction tradition, and inconsistency measure as a natural-number count. Two risk locations remain, mapped explicitly so the .thy writing knows where to look.

Oraclizer Core ⋅ May 08, 2026

Bridging Safety and Liveness: A Prelude to Compositional Verification

Two verification results now sit in our Isabelle/HOL repository: safety and liveness, proven independently. The harder task begins now. How do we compose them without losing each strength? This post records design choices we weigh before the composition proof begins: the abstraction level, the Canton interface, and the convergence claim we intend to make.

Oraclizer Core ⋅ Apr 19, 2026

Byzantine Fault Liveness, Discharged: What Properties 1 and 2 Together Guarantee

Property 2 of Oraclizer's formal verification program is complete. Byzantine fault liveness, mechanized in Isabelle/HOL under f<n/3, discharges the honest-node assumption that Property 1 implicitly carried. The combined_safety_liveness theorem is not a conjunction but an assume-guarantee discharge that lifts conditional safety into an unconditional guarantee.

Oraclizer Core ⋅ Apr 10, 2026

Proving D-quencer Liveness under Byzantine Faults: The Journey

Property 2 sorry elimination is complete. Six proof obligations and eight latent bugs across Priority_Resolution.thy and DQuencer_Instance.thy, resolved through nine build attempts. This post documents the reality of Isabelle/HOL formal verification where the hardest problems were tooling-related, and a two-character fix became the final build blocker.

Oraclizer Core ⋅ Apr 05, 2026

Building the Formal Model: Priority Resolution and Byzantine Tolerance in Isabelle/HOL

Property 2 modeling begins. Priority_Resolution.thy defines three domain-independent locales for deterministic selection, deadlock-free locking, and starvation freedom. DQuencer_Instance.thy instantiates them into the regulatory domain with nat-tuple lexicographic ordering and BFT consensus abstraction. Five sorry remain; zero in the instance file.

Oraclizer Core ⋅ Apr 02, 2026

Defining D-quencer Liveness under Byzantine Faults: Determinism, Deadlock Freedom, and Starvation Freedom

Property 1 proved safety with OSS modeled as a single honest entity. Property 2 extends the verified model with Byzantine fault verification: three liveness properties under f < n/3 Byzantine nodes. Determinism, deadlock freedom, and starvation freedom are formalized as domain-independent Isabelle/HOL locales reusable beyond regulatory systems.

Oraclizer Core ⋅ Mar 29, 2026

Cross-Domain State Preservation: What Was Proven and What It Means

Oraclizer's cross-domain state preservation theory is mathematically proven. Submitted to the Archive of Formal Proofs (AFP) and open-sourced on GitHub. A regulatory action on one chain is faithfully preserved across all connected chains, verified for every possible case by machine-checked proof. Not an audit. Not a test. Mathematical proof.

Oraclizer Core ⋅ Mar 27, 2026

Proving Cross-Domain State Preservation: The Journey

The core theorem regulatory_homomorphism is proven without sorry. Three lessons from the proof journey: fold-to-lambda redesign that improved both tractability and semantic accuracy, four failed attempts at existential quantification in Isabelle, and the 11 auxiliary lemmas that built the infrastructure for the 7-step proof.

Oraclizer Core ⋅ Mar 18, 2026

Formalizing Cross-Domain State Preservation in Isabelle/HOL

Three decisions shaped the state preservation model: replacing partial synchrony with atomic sync, constructing a 4-tier locale hierarchy in State_Preservation.thy, and discovering that valid_state emerges as an inductive invariant. This documents every modeling choice behind 1,436 lines of Isabelle/HOL.