2025/03/10 by Fabiański, Grzegorz, Stefański, Rafał, Litos, Orfeas Stefanos Thyfronitis · 1 citation
#Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2503.07200
In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We provide a custom implementation of (a simplification of) LN, express the desired security goals and, for the first time, we provide a machine checkable proof that they are upheld under every scenario, all in an integrated fashion. We build our system using the Why3 platform.