Skip to main content

Milad Ketab Ghale Haji Ali
Proof Engineer

Research Interests

Long ago Milad replaced the mysterious TRUTH by proof-objects and became mindful of practicality as much as the correctness. After his PhD at ANU, he decided to 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.



Served by Apache on Linux on seL4.