Oraclizer Core

Three Layers of Cross-Border Regulatory Conflict in Tokenized Securities

Cross-border tokenized securities do not face one regulatory problem. They face three interacting conflict layers: settlement cycle mismatch between T+1 and T+2 regimes, KYC and AML incompatibility across jurisdictions, and the non-atomic propagation of regulatory action across the domains where an asset exists simultaneously.

Oraclizer Core ⋅ Apr 12, 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 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

Safety and Liveness of Cross-Domain State Preservation: Now on arXiv

Oraclizer's combined Property 1+2 formal verification paper is now on arXiv. The Isabelle/HOL proof unifies cross-domain state preservation (safety) with BFT consensus liveness under Byzantine faults (f below n/3) into a single unified result, published with full source code, a 46-page proof PDF, and seven reusable domain-independent locales.

Oraclizer Core ⋅ Apr 07, 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

We Proved It: Cross-Domain State Preservation, Formally Verified

Oraclizer's first formal verification property is complete. Cross-domain state preservation, the guarantee that a regulatory state change on one chain is faithfully preserved across all connected chains, has been mathematically proven in Isabelle/HOL. Submitted to the Archive of Formal Proofs (AFP) and open-sourced on our first official GitHub repository.

Oraclizer Core ⋅ Mar 27, 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

SCBA air cylinder pressure gauge showing remaining capacity in the green zone with yellow and red alert zones ahead, representing the node incentive pool reserve levels and three-stage emergency protocol thresholds.

Revenue-to-Reward Conversion: The Sustainability Engine

How do block rewards and oracle fees converge into sustainable node compensation? This study designs a 2-Tier Node Incentive Pool with exponential decay, where the reward pool splits into Primary (2.1B OZ) and Sustainability Reserve (0.9B OZ), engineered for 7.6-year no-fee survival.

Oraclizer Core ⋅ Mar 22, 2026

Atomic State Binding: Formalizing Causal Consistency in Bidirectional Synchronization

Existing oracles transmit data bidirectionally through independent channels where each direction can fail independently, causing structural desynchronization. Atomic State Binding formalizes a stronger property: state transitions across domains succeed or fail as a single causal unit.