Dr Miki Tanaka is a Senior Proof Engineer at Trustworthy Systems Group. Miki has ample experience in system software verification using interactive theorem prover such as Isabelle/HOL and HOL4.