Thomas Pani

Thomas Pani

@thpani.bsky.social

Protocol Security Researcher :: https://blltprf.xyz | prev: @informalinc, @tuwien.at fuzzing, formal verification, bespoke security engineering

17 followers13 following9 posts

Thomas Pani
@thpani.bsky.social

Getting ready for my #Solidity #fuzzing workshop at @protocol.berlin 🔥 Join me to build a practical EVM smart contract fuzzer in Python and see how a Formal Methods viewpoint can guide your approach to smart contract security testing. #EVM #SmartContracts #Security

Thomas Pani
@thpani.bsky.social

1/ Distributed algorithms like blockchain consensus protocols are notoriously difficult 🤯 Too many combinations, too easy to miss bugs—fault-tolerance makes it worse. Tools like TLA+ & Apalache, Alloy, and CVC5 can help! Read our report: [arxiv.org/abs/2501.07958] 🧵

arxiv.orgTechnical Report: Exploring Automatic Model-Checking of the...We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique...
View full thread
Thomas Pani
@thpani.bsky.social

5/ Insights (3): Ultimately, checking the Alloy model with @arminbiere.bsky.social's Kissat SAT solver enabled verification of the largest state-space. Our approach demonstrates the power of combining tools to push the limits of what’s achievable in distributed protocol verification. ⚡️

Thomas Pani
@thpani.bsky.social

1/ Distributed algorithms like blockchain consensus protocols are notoriously difficult 🤯 Too many combinations, too easy to miss bugs—fault-tolerance makes it worse. Tools like TLA+ & Apalache, Alloy, and CVC5 can help! Read our report: [arxiv.org/abs/2501.07958] 🧵

arxiv.orgTechnical Report: Exploring Automatic Model-Checking of the...We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique...
View full thread
Thomas Pani
@thpani.bsky.social

3/ Insights (1): Specs in TLA+, Alloy, and SMT at various abstraction levels let us exhaustively check Accountable Safety for parameters reasonably large for verification. Extensive experiments, lasting up to 16 days, found no counterexamples—boosting confidence in the protocol’s safety. 🚀

Thomas Pani
@thpani.bsky.social

4/ Insights (2): Combining tools was pivotal. Refining the spec in TLA+ deepened our understanding of the protocol and shaped abstractions. Generating configurations like justified/finalized checkpoints was much easier with TLA+ and Alloy than with the initial Python spec. 🧠

Thomas Pani
@thpani.bsky.social

1/ Distributed algorithms like blockchain consensus protocols are notoriously difficult 🤯 Too many combinations, too easy to miss bugs—fault-tolerance makes it worse. Tools like TLA+ & Apalache, Alloy, and CVC5 can help! Read our report: [arxiv.org/abs/2501.07958] 🧵

arxiv.orgTechnical Report: Exploring Automatic Model-Checking of the...We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique...
Thomas Pani
@thpani.bsky.social

2/ We analyzed Accountable Safety, a critical property of the 3SF protocol, using formal methods tools and rigorous specifications. The protocol was designed by Francesco D’Amato, Roberto Saltini, Thanh-Hai Tran, and Luca Zanolini. Check out their exciting work: ethresear.ch/t/3-slot-fi...

ethresear.ch3-Slot-Finality: SSF is not about "Single" Slot3-Slot-Finality: SSF is not about “Single” Slot Authors: Francesco D’Amato, Roberto Saltini, Thanh-Hai Tran, Luca Zanolini TL;DR; In this post, we introduce 3-Slot Finality (3SF), a protocol designed to finalize blocks proposed by an honest proposer within 3 slots when network latency is bounded by a known value \Delta – even if subsequent proposers might be dishonest – while requiring only one voting phase per slot. This approach contrasts with previously proposed protocols for Single-Slot Fin...

You are up to date.