Talks and Lectures

• How model checking can help build trust in distributed protocols like Single Slot Finality at DevCon 2024, watch on youtube. Bangkok, Thailand, November 2024.

• Panel on Formal verification in the Ethereum Protocol: Current Status and Future Directions at DevCon 2024, watch on youtube. Bangkok, Thailand, November 2024.

• Specification and Model-checking of the ZKsync Governance Protocol at DeFi Security Summit 2024, watch on youtube. Bangkok, Thailand, November 2024.

• Pragmatic bounded model checking for TLA+ with Apalache at 16^th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE24). Prague, Czechia, October 2024.

• Apalache Tutorial [pdf] at TLA+ Community Meeting 2024, co-located with Formal Methods 2024, Milan, Italy, September 2024.

• Finding Bugs for Fun & Profit with Informal Systems. A 4-hour workshop at Cosmoverse 2023. Istanbul, Türkiye, October 2023. Together with Tesnim Abdellatif and Josef Widder.

• Lectures on Quint, TLA+, and Apalache at the VTSA’23 summer school. VTSA23 Lecture material. Nancy, France, August 2023.

• Quint at Gateway to Cosmos. Prague, Czechia, June 2023.

• Apalache: symbolic model checker for TLA+. Extended version of the talk at TLA+ tutorial, co-located with DISC 2021. Online, October 2021.

• How TLA+ and Apalache Helped Us to Design the Tendermint Light Client. Interchain Conversations 2020. Online, December 2020.

• Model-based testing with TLA+ and Apalache, with Andrey Kupriyanov. TLA+ Community Event 2020. Online, October 2020.

• Type inference for TLA+ in Apalache, with Jure Kukovec. TLA+ Community Event 2020. Online, October 2020.

• Formal Spec and Model Checking of the Tendermint Blockchain Synchronization Protocol 2nd Workshop on Formal Methods for Blockchains. Online, July 2020.

• Tutorial at DISCOTEC/FORTE 2020, FORTE20 - pdfs + video. Online, June 2020.

• Tutorial at VMCAI Winter School 2020: VMCAI20 - pdf. Louisiana, USA, January 2020.

More talks to be found in my CV.