3 papers
cs.LO2023
Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
Franck Cassez, Joanne Fuller, Milad K. Ghale +2
The Ethereum protocol implements a replicated state machine. The network participants keep track of the system state by: 1) agreeing on the sequence of transactions to be processed…
cs.LO2022
Deductive Verification of Smart Contracts with Dafny
Franck Cassez, Joanne Fuller, Horacio Mijail Anton Quiles
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our…
cs.PL2021
Formal Verification of the Ethereum 2.0 Beacon Chain
Franck Cassez, Joanne Fuller, Aditya Asgaonkar
We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethere…