Mechanized Proof for the Libra Blockchain

Date:

This talk presents formal methods work on the Diem (formerly Libra) blockchain, including a formalization of the safety of consensus in Coq.

The associated development can be found at the Novi Research repo.