F*

F*（英讀：F star）係一個由微軟研究院同埋INRIA主導開發嘅、基於ML嘅依賴類型函數式程式語言，主要用喺程式嘅形式化驗證。