[Dewie]

So what did they do? Write the code in C and then proved it with Isabelle/HOL? Extracted C code from Isabelle/HOL?