11-14, 09:45–10:15 (Asia/Bangkok), Classroom D
Validating Labeled State transition and Message production systems (VLSMs) provide a general approach to modeling and verifying faulty distributed systems. With formal definitions of validation and equivocation, we are able to prove that for systems of validators, the impact of Byzantine components is indistinguishable from the effect of the introduction of corresponding equivocating components. All of the results presented in this talk have been formalized and checked in the Coq proof assistant
Vlad Zamfir is a renowned blockchain researcher and software developer who has made significant contributions to the Ethereum network. He is widely recognized for his work on the proof-of-stake (PoS) consensus algorithm.