Skip links

Type and hit enter

Subscribe
Oraclizer Research

Proofs

Proving Cross-Domain State Preservation: The Journey

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

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.
Oraclizer Core ⋅ Mar 18, 2026
Defining Cross-Domain State Preservation: What Are We Proving?

Defining Cross-Domain State Preservation: What Are We Proving?

This article documents our semi-formal specification for Property 1, cross-domain state preservation homomorphism. We define five regulatory states and seven actions, fix a partially synchronous network with honest nodes, introduce preemptive locking, and explain renaming the Regulatory State Functor to the Cross-Domain State Preservation Functor as a generic locale.
Oraclizer Core ⋅ Feb 28, 2026
Higher-Order Logic as a Design Language: Why Our Verification Requires HOL

Higher-Order Logic as a Design Language: Why Our Verification Requires HOL

Cross-chain regulatory homomorphism demands quantification over state transition functions, a statement structurally impossible in first-order logic. This article derives the necessity of Higher-Order Logic from Oraclizer's verification target, introduces Isabelle/HOL through regulatory state modeling, and grounds the Regulatory State Functor in category theory.
Oraclizer Core ⋅ Feb 25, 2026
Why We’re Starting Formal Verification: Applying Our Own Standard

Why We’re Starting Formal Verification: Applying Our Own Standard

We argued RWA infrastructure needs mathematically provable compliance. Now we apply that standard to ourselves. This is the first entry in Oraclizer's formal verification journey: using Isabelle/HOL to verify cross-chain regulatory state synchronization preserves structural correctness at the design level, before any production code exists.
Oraclizer Core ⋅ Feb 21, 2026
2