4 ms·

I believe Isabelle/HOL was used to prove seL4 correct. So it is indeed an industrial strength tool.