F*：Microsoft Researchが開発する証明指向プログラミング言語

F*: A general-purpose proof-oriented programming language

F*（エフスター）は、依存型とSMTソルバーによる証明自動化、タクティクに基づく対話的定理証明を組み合わせた、汎用の証明指向プログラミング言語です。純粋関数型と作用型の両方のプログラミングをサポートし、デフォルトでOCamlにコンパイルされます。さらに、KaRaMeLやValeツールチェーンを用いて、F#、C、Wasm、アセンブリへの抽出も可能です。F*はMicrosoft ResearchとInriaによって活発に開発されており、Apache 2.0ライセンスで公開されています。