...
Our method relies on using EventML. EventML cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements.
To create correct-by-construction code we:
...