Thomas Pani
@thpani.bsky.social
Protocol Security Researcher :: https://blltprf.xyz | prev: @informalinc, @tuwien.at
fuzzing, formal verification, bespoke security engineering
fuzzing, formal verification, bespoke security engineering
Abstract 👇👇👇
25-Minute Solidity Fuzzer: Fuzzing Smarter, Not Harder Protocol Berg v2
**Fuzzing and Formal Methods** are often seen as competing approaches to smart contract security. In this **hands-on workshop**, we combine insights from both, allowing participants to build a **minim...
cfp.protocol.berlin
May 23, 2025 at 10:00 AM
Abstract 👇👇👇
6/ Huge thanks to co-authors @k0nn0v.bsky.social, Jure Kukovec, Roberto Saltini, and Thanh-Hai Tran! We are deeply grateful to Luca Zanolini and Francesco D’Amato for the fruitful discussions and @ethereum.foundation for supporting our work under the 2024 Academic Grants Round!
January 17, 2025 at 10:23 AM
6/ Huge thanks to co-authors @k0nn0v.bsky.social, Jure Kukovec, Roberto Saltini, and Thanh-Hai Tran! We are deeply grateful to Luca Zanolini and Francesco D’Amato for the fruitful discussions and @ethereum.foundation for supporting our work under the 2024 Academic Grants Round!
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. ⚡️
Our approach demonstrates the power of combining tools to push the limits of what’s achievable in distributed protocol verification. ⚡️
January 17, 2025 at 10:23 AM
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. ⚡️
Our approach demonstrates the power of combining tools to push the limits of what’s achievable in distributed protocol verification. ⚡️
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. 🧠
January 17, 2025 at 10:23 AM
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. 🧠
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. 🚀
January 17, 2025 at 10:23 AM
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. 🚀
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...
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...
3-Slot-Finality: SSF is not about "Single" Slot
3-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...
ethresear.ch
January 17, 2025 at 10:23 AM
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...
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...