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_microkern

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_assurance:_seL4 https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...