Skip links

Type and hit enter

Subscribe
Oraclizer Research

Proofs

When Regulatory Actions Do Not Commute: Order, Outcome, and Sixty Normal Forms

When Regulatory Actions Do Not Commute: Order, Outcome, and Sixty Normal Forms

Enforcement standards define what a freeze or a confiscation does, and say nothing about what happens when two commands overlap. Regulatory action composition closes that gap in Isabelle/HOL: twenty-one action pairs split into twelve commuting and nine not, each non-commuting pair with a witness, and exactly sixty state transformations behind unbounded sequences.
Oraclizer Core ⋅ Jul 31, 2026
The Cross-Domain State Preservation Functor: What It Closed, and What It Was For

The Cross-Domain State Preservation Functor: What It Closed, and What It Was For

The cross-domain state preservation proofs are closed: homomorphism, functor completion, a natural-transformation tower, and unconditional bounded convergence. Ten theory files, zero sorry. The harder work was catching what passes a prover while saying nothing: a trivial functor, a bypassed threshold, a witness outside the roster. Each retreat left the rest firmer.
Oraclizer Core ⋅ Jul 16, 2026
Three Category Axioms, One Proved Functor

Three Category Axioms, One Proved Functor

A research-journal account of mechanizing the functor laws and the degree-hierarchy natural transformation in Isabelle/HOL, where the obstacles were almost never the mathematics. The measure decrease I feared closed at once; a reserved keyword broke seven builds; a finiteness clash forced a redefinition; and the code overturned my belief that glue gives validity.
Oraclizer Core ⋅ Jun 06, 2026
Designing Compositional State Assurance: Three Locales and One Glue

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

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

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 below 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

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

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
1