He probably mean a heavy focus on type theory. It has been used in formal verification as a prototype tool [1].

[1]: https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...