Showing 2025Show all
2 papers · 1 filter
cs.CR2025
A Formally Verified Lightning Network
Grzegorz Fabiański, Rafał Stefański, Orfeas Stefanos Thyfronitis Litos
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…
cs.FL2025
Polyregular Model Checking
Aliaume Lopez, Rafał Stefański
We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean va…