Open Problems in Rollups
Talk, Ethereum Engineering Group Meetup, Sydney, Australia
A youtube video with a presentation on open problems in rollup technology. 
Talks and Blog Posts
How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
Researchers at ConsenSys designed a machine-checkable correctness (and termination) proof for the Eth2 deposit contract, ensuring that the deposit contract is correct and free of runtime errors.
Verification of the Deposit Contract in Dafny
Talk, Ethereum Engineering Group Meetup, Sydney, Australia
A youtube video with a presentation on our formal verification of the deposit contract. 
Formally Verifying the Ethereum 2.0 Phase 0 Specifications
An update from ConsenSys R&D on their effort to bring trustworthiness to the Beacon Chain and the core foundations of Eth2.
Verification of Eth2.0 in Dafny
Talk, Ethereum Engineering Group Meetup, Sydney, Australia
A youtube video with a presentation on our formal verification of the Eth2.0 specs. 