Page History

...

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

Using EventML's correct-by-construction synthesizer we generate code from the specification.

...