Can You Prove Your Smart Contract Is Correct?
Meet Blaster - a tool for automated formal verification of Cardano smart contracts.
Join Romain Soulat and Jean-Frédéric Etienne from IOG to see how Blaster can automatically prove that a contract meets its specification - or produce a concrete counterexample when it doesn’t.
We’ll explore:
• Lean 4 & automated proofs
• UPLC, CEK & ledger formalization
• Writing contract specifications
• Live demo: proofs & counterexamples
• What’s next for Blaster
• Q&A
Curious about smart contract security, formal verification, or high-assurance development? Come see Blaster in action and bring your questions!
Tuesday, 09 October 2026
08:00 UTC
Developers Office Hours #82 | AddEvent
Missed a session? View the recordings here.
You can subscribe directly to the calendar here: Cardano Developers | AddEvent
Join the discussion below! We’ll update this thread with the recording link as soon as it’s live.
