...
For more details about the example below see Mark's presentation at the May 2012 CRASH meeting.
Example with Consensus
In this example we will look at Paxos consensus, focusing on specifying the Scout protocol.
...
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
...