Skip to main content

Milad Ketab Ghale Haji Ali
Proof Engineer

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..

Contact Details

More contact information is available at the Contact page.

Photo of Milad Ketab Ghale Haji Ali