Research Interests

Long ago Milad divorced the mysterious TRUTH and sided with proof-objects. He became mindful of practicality as much as the correctness. After his PhD at ANU, he join TS doing proof engineering where he can practice the best of formal method techniques and tools for the sake of both the correctness and practicality.

Currently, his work concerns the CASE project where he is validating a translation of seL4 system initializer from its Isabelle specification into CakeML language..