Proofs

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.

Oraclizer Core ⋅ Mar 18, 2026

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

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

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

Subscribe