“Casper the friendly ghost”

Correct-by-construction consensus safety

By: Vlad Zamfir

February 17

th

, 2017 

EDCON 

2

Outline

Set up:

What is correct-by-construction protocol design?

Overview of consensus protocol basics

Binary Casper data structures + definitions

Estimate safety

3

Outline

Consensus safety proof

The correct-by-construction Casper consensus decision rule  
using an estimate safety oracle

Proof of consensus safety of the Casper consensus decision 
rule using an estimate safety oracle

4

Outline

Completing the specification

The ideal adversary as an implementation of the safety oracle

Lower bounds on safety

An ideal adversary for the lower bound on safety

5

Outline

Roadmap for the correct-by-construction Casper

Q + A

Conclusion

So, what is correct-by-constrution protocol design?

7

“The Normal Way”

1) Formally specify the protocol

2) Define properties that protocol must satisfy

3) Prove that the protocol has given properties

8

“The Correct-by-Construction Way”

1) Formally but partially specify the protocol

2) Define properties that protocol must satisfy

3) Derive more of the protocol in a way that is 
proven to satisfy them

9

“The Normal Way”

1) Formally and completely specify the protocol

2) Define properties that protocol must satisfy

3) Prove that the protocol has given properties

The goal is that giving a proofs of the 
protocol’s correctness is almost trivial.