Consensus algorithms are fundamental to the operation of distributed systems, underpinning applications ranging from blockchain technology to distributed databases. However, ensuring the correctness and resilience of these algorithms remains a significant challenge. This paper presents a novel approach to formally verifying consensus algorithms using distributed simulation. We propose a framework that allows for the emulation of a consensus algorithm on a distributed network, facilitating the detection of potential vulnerabilities and failures before deployment. The core of our method involves systematically simulating the algorithm under various failure scenarios, capturing the algorithm's behavior and identifying deviations from expected outcomes. This approach offers a practical and scalable solution for verifying consensus algorithms in real-world distributed systems, contributing to increased system reliability and security. The simulation framework utilizes the following key elements: a model of the consensus algorithm, a distributed network simulator, and a verification engine that analyzes the simulation results. We demonstrate the feasibility and effectiveness of our method through a detailed example, highlighting its potential for broad application in the verification of diverse consensus algorithms.
This paper presents a novel approach to distributed constraint satisfaction (CS) algorithms by leveraging blockchain technology for verification. The core challenge in distributed CS lies in ensuring the correctness and reliability of the algorithms across multiple nodes. Existing solutions often rely on centralized trust models, which are vulnerable to manipulation and single points of failure. Our proposed system addresses this by employing a decentralized architecture where each node executes a CS algorithm, and the resulting solutions are cryptographically verified through a blockchain. This creates an immutable audit trail, guaranteeing the integrity of the process and fostering trust among participants. The system uses a distributed consensus mechanism to maintain the blockchain and ensures that any deviation from the expected solution will be flagged. This approach significantly enhances the security, reliability, and transparency of distributed CS, opening possibilities for applications in areas like smart grids, supply chain management, and decentralized autonomous organizations (DAOs). The key innovation resides in the combination of distributed computation with verifiable blockchain records, offering a robust and trustworthy solution for complex problem-solving scenarios.
Tokenized real-world assets trade continuously on public blockchains, but thevenues that price their underlyings do not. For roughly two-thirds of wall-clocktime, an on-chain protocol must value collateral against a market that is shut. This record accompanies "Coverage Inversion: Calibration-Transparent Fair-ValueOracles for Closed-Market Hours". The paper inverts the conventionalpoint-plus-confidence oracle interface: the target coverage level tau becomes apublished product input, and every served price band carries a calibrationreceipt that a third party can reconstruct from public data. CONTENTS The paper (67 pages) and the LaTeX source arXiv compiles. A reference implementation in three languages — the Python serving path, its Rust port (pinned to the Python by a 329-case parity harness), and the Anchor programs for the on-chain publish path. The calibration artefacts: the 20 deployment scalars that define the served bands, including the SHA-256-stamped frozen artefact used for out-of-sample validation. The public band archive: an append-only record of bands actually served, with Saturday width commitments published before Monday's open, so the claims can be audited after the fact rather than taken on trust. EVIDENCE Two closed-market panels over the same ten US-listed tickers, 2014-2026: 5,996 weekend windows (Friday close to Monday open) and 22,624 overnight windows (close to next open). The headline weekend result is held out by leave-one-symbol-out cross-validation at tau = 0.95: realised coverage 0.9497 +/- 0.0128, every fold passing Kupiec. On a 40-cell symbol-by-tau grid the architecture passes 40 of 40 Kupiec tests, against 31 of 40 for the strongest practitioner baseline (GARCH-t). The same architecture, with only its gap selector changed, carries from weekends to overnight gaps — calibration transparency is a property of closed market hours generally, not of weekends specifically. Because an earnings release has a publicly known date and session, the band widens deterministically ahead of it. No incumbent oracle exposes calendar-conditioned coverage. LICENSING This record is CC BY 4.0. The source code in the reference-implementation archive is Apache-2.0 and ships its own LICENSE file, which governs that archive.