1. 3

Instead of ML, they extract Coq programs to C language for better performance and much smaller TCB. Whitepaper is here. Github is here.

  1.