...
In this example we will look at Paxos consensus, focusing on specifying the Scout protocol.
Step 1 - We write the Scout specification in EventML
Step 2 - Generate the Inductive Logical Form (ILF)from the Scout specification
Using EventML's interface with Nuprl, we generate the ILF. If there are any issues with the proof we revise the specification and reiterate the process with the ILF.
Step 3 - Synthesize Consensus Code
...
ShadowDB is a replicated database, created by Nicolas Schiper, on top of a synthesized consensus core. The primary defines the order in which transaction updates are applied. When crashes occur, consensus is used to reconfigure the set of replicas and agree on a prefix of executed transactions.
