...
Step 1 - We write the specification in EventML
Step 2 - Generate the Inductive Logical Form (ILF)
...
Using EventML's correct-by-construction syntesizer synthesizer we generate code from the specification.
...
ShadowDB is a replicated database we created on top of a synthesized consensus core. The primary defines the order in which transaction updates are applied. When crashes occur, consensus is used to reconfigure the set of replicas and agree on a prefix of executed transactions.
