...
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 code
Using EventML's correct-by-construction syntesizer we generate code from the specification.
...