adic-lean-proof
GhostDrift ADIC Lean Proof
A Lean formalization of a core lemma in ADIC (Advanced Data Integrity by Ledger of Computation), developed by the GhostDrift Mathematical Institute.
Overview
This repository contains a machine-checkable proof artifact for a core safety property used in the ADIC verifier architecture.
The formalization corresponds to the following research work:
Deterministic Linear-Time Verification of Interval Programs via Quantifier-Free Fixed-Point Integer Certificates
Proof File
The Lean formalization is provided in:
Lean Verification Result
The core lemma of ADIC has been formally verified using Lean 4.
Verification
To verify the proof locally, run:
lake build
Purpose
This repository is released as a formal proof artifact supporting the theoretical foundations of ADIC.
Related Paper
The theoretical framework and results associated with this Lean formalization are described in the following paper:
Zenodo (archival version):
https://zenodo.org/records/18897322
This repository contains a machine-checked Lean formalization of selected core components related to the integer replay verification framework discussed in the paper.
License
MIT License