...
Step 2 - Generate the Inductive Logical Form (ILF)from the Scout specification
Using Here EventML 's interface with Nuprlinterfaces with Nuprl's formal library and theorem prover. Using the distributed prover, we generate the ILFa proof of the protocol which results in a readable Inductive Logical Form. If there are any issues with the proof we revise the specification and reiterate the process with the ILF.
...
Engaging our diversity in classes and state machines we generate multiple verified versions of the code. Then the final step before deployment is to test the code in the EventML simulator. The result is a correct-by-construction synthesized version of Paxos.
Example Deployment: ShadowDB
...