F*: 汎用証明指向プログラミング言語
概要
F* は、依存型、SMT ソルバー、および戦術ベースの対話的定理証明を通じて、純粋関数型および副作用のあるプログラミングをサポートする汎用証明指向プログラミング言語です。
この言語は F* で実装され、OCaml を使用してブートストラップされます。そのコア設計は、豊富な仕様を表現するために依存型に依存し、証明の自動化は SMT ソルバーと対話的戦術言語によって提供されます。F* プログラムは関数型スタイルで書くことも、状態、例外、または並行性などのエフェクトを用いて書くこともでき、同じ言語でプログラムとその正当性証明の両方を記述します。
コンパイルターゲット
F* プログラムはデフォルトで OCaml にコンパイルされ、さらに F#、C、WebAssembly、および KaRaMeL と Vale を介した検証済みアセンブリへの抽出パスがあります。
デフォルトでは、F* コンパイラは OCaml ランタイムにリンクできる OCaml コードを出力します。KaRaMeL ツールは F* のサブセット（Low* も含む）を C または WebAssembly に抽出します。Vale ツールチェーンは低レベルの F* フラグメントをアセンブリ言語に抽出し、パフォーマンスクリティカルなコードの検証を可能にします。これらの抽出メカニズムにより、同じソースから複数のバックエンドをターゲットにしながら、関数的正しさの保証を維持できます。
インストールと配布
F* は Apache 2.0 ライセンスでリリースされ、GitHub リリースで Windows、Linux、macOS 用のバイナリを提供し、さらに OPAM、Docker、Nix、およびソースビルドも提供します。
ユーザーは GitHub の F* リリースページからプリビルドされたバイナリをダウンロードできます。代替インストール方法としては、OPAM パッケージ、Docker イメージ、Nix 式、または INSTALL.md の手順に従ったソースからのビルドがあります。すべての配布チャネルは、Microsoft Research、Inria、およびコミュニティの F* 開発チームによって維持されています。
学習リソース
F* の主要な学習教材は、オンラインブック『Proof-oriented Programming In F*』、それに加えて Low* チュートリアルおよびシーズナルスクールからのさまざまなコース教材です。
ブック『Proof-oriented Programming In F*』は定期的に更新され、F* ウェブサイトで PDF として利用可能です。伴うチュートリアルページでは、スナップショットとブラウザで試せる演習が提供されます。別途、Low* チュートリアルがあり、これは KaRaMeL を介して C にコンパイルされる F* の低レベルサブセットをカバーします。Oregon Programming Language Summer School（2019、2021）、ECI 2019、EUTypes Summer School 2018 などのイベントからのコース教材もオンラインで公開されており、講義ノート、スライド、コード例が含まれています。
Low* サブセット
Low* は、KaRaMeL を介して C にコンパイルできる F* の低レベルサブセットであり、検証済みシステムズプログラミングを可能にします。
Low* は F* をシステムズコードに適したフラグメントに制限し、メモリレイアウトとインラインアセンブリへの直接制御を提供しながら、言語の依存型システムを保持します。Low* で書かれたコードは F* で正当性を証明した後、効率的な C に抽出でき、これにより検証済み暗号プリミティブ、パーサー、および OS コンポーネントの開発に適しています。
コミュニティとサポート
F* コミュニティは、GitHub Discussions、公開 Zulip フォーラム、低トラフィックのメーリングリスト、および月次 PoP Up セミナーを使用してコミュニケーションとサポートを行っています。
質問と告知は GitHub Discussions フォーラムで処理されます。公開 Zulip チャット（fstar.zulipchat.com）は主要なリアルタイムディスカッションの場として機能します。Google Groups メーリングリストは低トラフィックの告知のために存在します。F* PoP Up セミナーはユーザーと開発者の会合で、不定期に開催されますが、月次ペースを目指しています。メンテナーは fstar-maintainers@googlegroups.com に連絡できます。
産業および学術での利用
F* はいくつかの高保証プロジェクトで使用されており、特に Project Everest が顕著です。Project Everest は、Firefox、Linux カーネル、Python、mbedTLS、Tezos、ElectionGuard、Wireguard、Windows Hyper‑V、および ebpf‑for‑windows に配備された検証済み暗号ライブラリとパーサーを生成します。
Project Everest は HACL*（検証済み暗号ライブラリ）、ValeCrypt（検証済みアセンブリ暗号）、および EverCrypt（組み合わせプロバイダー）を開発します。EverParse はバイナリ形式の検証済みパーサーを生成します。これらの成果物は本番ソフトウェアに統合されています：Firefox は HACL* を TLS に使用し、Linux カーネルは HACL* curve25519 コードを含み、Python の cryptography ライブラリは HACL* を組み込み、mbedTLS は EverCrypt をバンドルし、Tezos は HACL* に切り替え、ElectionGuard は EverCrypt に依存し、Wireguard は HACL* を暗号操作に使用し、Windows Hyper‑V は EverParse が生成したパーサーをネットワークパケットに使用し、ebpf‑for‑windows プロジェクトは EverParse を eBPF プログラムのロードに使用します。
研究の基盤
F* に関する研究は、言語設計、意味論とエフェクト、セキュリティと暗号、システムズ、パース、プログラミングとプログラム解析、および AI アシストプログラミングにわたり、プロジェクト書誌に多数の査読済み論文が引用されています。
主要な著作には、POPL 2016 論文 "Dependent Types and Multi-monadic Effects in F*"（コア言語を記述）、ICFP 2017 論文 "Verified Low-level Programming Embedded in F*"（Low* を導入）、POPL 2019 論文 "A Verified, Efficient Embedding of a Verifiable Assembly Language"（Vale を提示）、および ESOP 2019 論文 "Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms"（メタプログラミングシステムを記述）があります。その他の論文では、Dijkstra モナド、Steel と SteelCore の同時分離論理、USSL と PulseCore、および暗号、システムズ、パース、およびプログラミング言語実装におけるさまざまなアプリケーション固有の検証が扱われています。
セキュリティと暗号における応用
F* は、TLS 1.3、QUIC、Signal、ポスト量子 TLS、およびさまざまな認証暗号構成の暗号プロトコルと実装の検証に適用されています。
注目すべき検証済み成果物には、TLS‑1.3 レコードレイヤー（S&P 2017）、HACL*（CCS 2017）、EverCrypt（S&P 2020）、HACL×N（CCS 2020）、QUIC レコードレイヤー（S&P 2021）、DICE 測定ブート（USENIX Security 2021）、DY* フレームワークによるシンボリックプロトコル分析（Euro S&P 2021）、Noise* ライブラリによるセキュアチャネルプロトコル（S&P 2022）、TreeSync（MLS 用、USENIX Security 2023）、および Comparse（プロトコル認識パース、CCS 2023）があります。最近の研究では、F* への翻訳を介した Rust TLS‑1.3 実装の検証も行われています（CCS 2025）。
システムズにおける応用
F* は、メモリアロケータ、サンドボックス、データ整合性モニター、および並行キー値ストアの検証に使用されています。
例として、検証済み WebAssembly サンドボックス（USENIX 2022）、FastVer と FastVer2 によるデータ整合性モニタリング（SIGMOD 2021、CPP 2022）、ECOOP 2024 の Pipit によるリアクティブリアルタイムシステム、および Steel で検証されたハードened 並行メモリアロケータ StarMalloc（SPLASH 2024）があります。
パースにおける応用
F* は、EverParse と ASN1* のような検証済みパーサージェネレーターを駆動し、CBOR、CDDL、COSE、および ASN.1 DER などのバイナリ形式の検証済み C パーサーを生成します。
EverParse は USENIX Security 2019 で発表され、後に PLDI 2022 の Hyper‑V パケットパーサーのハードニングに使用されました。ASN1* は検証済み ASN.1 DER パースを提供します（CPP 2022）。最近の研究では、F* で CBOR、CDDL、および COSE を形式化し、Pulse（CCS 2025）で検証済みパーサーとフォーマッターを開発しています。
プログラム、プログラム証明、およびプログラム解析における応用
F* は、可逆回路の検証済みコンパイル、セッションタイプ付きマルチパーティプロトコル、抽象インタープリター、法律向けドメイン固有言語、および Rust と OCaml コードの検証をサポートしています。
注目すべき成果には、可逆回路の検証済みコンパイラ（CAV 2018）、マルチパーティプロトコル用 Session*（OOPSLA 2020）、F* で検証された抽象解釈フレームワーク（SAS 2021）、法律向け Catala 言語と検証済みコンパイラ部分（ICFP 2021）、Merkle Patricia ツリーの検証（arXiv 2021）、Rust を F* に翻訳して関数的正確性を確保する Aeneas（ICFP 2022）、SteelCore を量子分離論理に適応させる Q*（PlanQC 2022）、未検証コードとの安全な相互作用のための SecIO* と SecRef*（POPL 2024、ICFP 2025）、および F* と Low* で検証された OCaml の機械的に検証済みガベージコレクタ（JAR 2025）があります。
AI アシストプログラミングの取り組み
最近の研究では、ニューラル合成と AI エージェントを用いて F* プログラムと証明の生成を自動化し、さらに自然言語からバイナリ形式の仕様を導き出そうとしています。
ICSE 2025 論文 "Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming" は、プログラムと証明の合成のためのモデルを訓練するために大規模な F* コードコーパスをキュレートしています。arXiv 論文 "3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers" は、RFC と例を形式仕様に変換し、EverParse で使用できるエージェントを開発しています。
Hacker News におけるコミュニティフィードバック
Hacker News の投稿へのコメントでは、構文例の可視性向上への欲求、産業採用への問い合わせ、およびコンパイラ検証と低レベルプログラミングへの言語の適合性について議論されました。
"Clicked like 5 pages and never found 1 code example. Idk why languages don't have their syntax in a sandbox front-and-center on the home page. It's like a video game site with zero screenshots or videos (also rampant). New programming languages I want 2 things: 1. What does the syntax look like 2. Why would I use this language Talk about the proof logic, show the syntax, thank you" – @cyanregiment
"I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language." – @pvsnp
"https://fstar-lang.org/tutorial/" – @LelouBil
"I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages. Is this used in the industry ? And for what kind of software ?" – @LelouBil
"Guess responsive stylesheets can't be implemented without side effects..." – @boutell
"Would this language be useful for implementing compilers and formally proving things about them?" – @3lambda
"Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?" – @_doctor_love
"F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out. Does it get basic stuff like subtraction and u8 right, unlike Lean?" – @IshKebab
"- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust" – @vivzkestrel