
2026/08/02 21:31
F*:汎用証明指向プログラミング言語
RSS: https://news.ycombinator.com/rss
要約▶
Japanese Translation:
F* は、依存型と SMT/tactic ベースの自動化をサポートし、純粋な関数型コードとエフェクトを持つコードの両方を扱える汎用証明指向プログラミング言語です。デフォルトでは OCaml にコンパイルされ、KaRaMeL および Vale を通じて F#、C、WebAssembly、アセンブリーへの抽出オプションも提供されます。Apache 2.0 ライセンスで GitHub にオープンソース化されており、プロジェクトは F* で実装され OCaml でブートストラップされています。開発は Microsoft Research、Inria、コミュニティ(Windows、Linux、macOS)によって推進されています。インストール方法としては、OPAM、Docker、Nix、ソースビルド(INSTALL.md 参照)、プリビルトリリースが利用可能です。学習リソースには「Proof-oriented Programming in F*」という書籍、Low* チュートリアル、2018 オフリッドで開催された EUTypes サマースクールなどのサマースクールの教材が含まれます。コミュニティへの参加は GitHub Discussions(推奨)統合された Zulip フォーラム低トラフィックのメーリングリスト、毎月開催される PoP Up セミナーを通じて可能であり、メンテナーは fstar-maintainers@googlegroups.com で連絡可能です。
Project Everest にインスピレーションを得た F* は、高信頼性の安全な通信ソフトウェアを支えています。派生プロジェクトには、C 言語による暗号原語を実装する HACL*、Vale を用いた検証済みアセンブリを提供する ValeCrypt、統一された検証済み暗号プロバイダーである EverCrypt、バイナリ形式の C パーサーを検証する EverParse が含まれます。これらのプロジェクトからのコードは、Mozilla Firefox、Linux カーネル、Python、mbedTLS、Tezos ブロックチェーン、ElectionGuard SDK、Wireguard VPN、Windows Hyper-V(Azure クラウドネットワークパケットの検証)、eBPF-for-Windows のプロダクション環境で展開されています。数学的証明と実用的なツールの組み合わせにより、F* は学術研究と現実世界の重要インフラを橋渡しし、複数のデプロイパスを提供しながら安全性の保証を損なわずに機能します。
本文
F* プログラミング言語入門ガイド
イントロダクション
F*(「F スター」と発音)は、以下の特性を持つ汎用的な証明志向型プログラミング言語です。
- 多様なアプローチの統合: 純粋な関数型プログラミングと、効果(Effect)を持つプログラミングを両方支援します。
- 強力な表現力: 依存型(Dependent Type)を活用し、SMT ソルバーに基づく証明自動化や、タクティクスベースの対話式定理証明を統合しています。
コンパイルと実装環境:
- デフォルトでは OCaml にコンパイルされます。
- KaRaMeL ツール:F# や C、Wasm へ抽出可能。
- Vale ツールチェーン:アセンブリ言語へも抽出可能。
- F* は OCaml を用いて自己構築(ブートストラップ)されています。
オープンソースであり、GitHub で公開されています(Microsoft Research, Inria, コミュニティが開発を担う)。
ダウンロードとインストール
F* は Apache 2.0 ライセンスの下で配布されています。以下の方法から入手可能です。
- Windows / Linux / macOS: GitHub のリリースページからバイナリを取得。
- パッケージマネージャー・コンテナ: OPAM、Docker、Nix からインストール可能。
- ソースビルド:
に記載の手順に従って構築することもできます。INSTALL.md
学習リソースと教材
オンライン書籍
『Proof-oriented Programming In F***』のオンライン書籍があります。ブラウザ上で例題や演習を試しながら読むことをお勧めします。
Low* チュートリアル
KaRaMeL によって C にコンパイル可能な、F* の低レベルサブセットであるLow*を扱うチュートリアルも用意されています。
コース資料と講義録
様々なカンファレンスや学校で開催される講座の資料は以下の通りです。
- Proof-oriented Programming Languages in F* (2021)
- オレゴン プログラミング言語 サマースクール(オンライン)
- 講義ノート、スライド、コード
- F と Meta-F を用いた形式的検証** (2019)
- ECI での講義およびチュートリアル
- 講義ノート、スライド、コード
- 正しさと安全性の検証のための低レベルコード (2019)
- オレゴン プログラミング言語 サマースクール
- 講義ノート、スライド、コード
- F によるプログラム検証* (2018)
- EUTypes サマースクール(マケドニア、オヒリッド)
- コース資料
コミュニティ参加方法
フォーラムと連絡先
質問やアナウンスメントは以下の場所で行われます。
- GitHub Discussions: 主要な議論場所(Slack から移行中)。
- Zulip: オンラインコミュニティへの統合を進める公開フォーラム。
- メーリングリスト:
(購読はこちら)。fstar-mailing-list - PoP Up Seminar: ユーザと開発者のための集会(原則 1 ヶ月に一度)。
- 保守者連絡先:
fstar-maintainers@googlegroups.com
利用状況レポート
貴プロジェクトで F* をご活用されている場合は、上記メーリングリストへお知らせください。
プロジェクト・イヴェレスト (Project Everest)
高信頼性かつ安全な通信ソフトウェア開発のための傘下プロジェクトです。主な派生プロジェクトには以下のものがあります。
| 項目 | 詳細 |
|---|---|
| HACL* | F* で書かれた高信頼性の暗号的原語ライブラリ(C へ抽出)。 |
| ValeCrypt | Vale (検証済みアセンブリ) フレームワーク内で形式証明された暗号実装。 |
| EverCrypt | HACL* と Vale を統合した単一暗号プロバイダ。 |
利用実績: Mozilla Firefox, Linux カーネル, Python, mbedTLS, Tezos, ElectionGuard, Wireguard など。
主要な応用分野と研究事例
EverParse
形式的に証明された F* から抽出された C コードによるパースアジェネレータです。
- 用途: Azure クラウドの全ネットワークパケット、Windows Hyper-V のパケットパースなど。
セマンティクスと効果に関する研究
F* の効果システム(ダイヒストアモノイドなど)に関する理論的基盤を確立した研究群です。
- ダイヒストアモノイド (POPL 2017, PLDI 2013): 計算のモノイドクラスに対して自動的に導出する手法。
- 関係検証フレームワーク (CPP 2018): プログラムまたは実行間に関する性質を証明するための基盤。
- SteelCore & PulseCore: 並列分離論理(SPL, PLDI 2025 など)の拡張と実装。
セキュリティと暗号への応用
検証済み暗号ライブラリやプロトコル実装に関する多数の研究があります。
- WYS*: 検証済み安全な多側計算のための DSL (POST 2017)。
- TLS 1.3 レコード層: Low* による検証済み実装と証明 (S&P 2017)。
- HACL×N: メタプログラミングによる汎用 SIMD 暗号化の実現 (CCS 2020)。
- DY*: F* を開発した暗号プロトコルに対するシンボリックセキュリティ分析フレームワーク。
- Noise, TreeSync, Comparse*: 安全通信チャネルや認証済みグループ管理、フォーマット解析の安全性証明。
システム・並列性への応用
ハードウェアレベルからの検証とシステム最適化に関する研究群です。
- WebAssembly サンドボックス: Low* と Rust における多言語ソフトウェアの検証 (USENIX 2022)。
- FastVer / FastVer2: データ整合性のコモディティ化と並列キーバリューストアの正しさ証明。
- StarMalloc: Steel で検証されたセキュリティ志向のメモリアロケーター (SPLASH 2024)。
パーシング・フォーマットへの応用
形式化されたデータ構造とパーサーの開発です。
- ASN1, CBOR, CDDL, COSE*: F* による形式化と Pulse/PulseCore を用いた安全なパースライブラリ。
- Rust 向け検証 (CCS 2025): Bert13 と Hax を使用した、TLS-1.3 や後量子機能の実装の安全性証明。
プログラミング・解析・言語設計への応用
言語理論やプログラム変換、抽象解釈に関する研究群です。
- ReVerC: 空間効率の高いリバーシブル回路コンパイラ (CAV 2018)。
- Session*: 多側プロトコル向けのセッション型プログラミング言語 (OOPSLA 2020)。
- Merkle Patricia Tree: OCaml から F* への移植と正しさ証明。
- PEEPUL: 複製データタイプ構築のフレームワーク (PLDI 2022)。
- SecRef*: 静的に検証された状態型プログラム間の安全な参照共有 (ICFP 2025)。
- Aeneas / Q / Pipit*: Rust の検証、量子分離論理、リアクティブシステムの埋め込み DSL など。
AI 支援型プログラミング
人工知能を用いたコード合成や仕様解析の研究です。
- 神経合成 (ICSE 2025): F* コードデータセットに基づくプログラムおよび証明の自動合成。
- 3DGen: 自然言語仕様のデータ形式パーサーの AI エージェントによる生成。
その他・基礎研究
- プログラミング言語のセマンティクス (ICSE-SEET 2023): 演算的、意味論的、公理的セマンティクスの教授体験。
歴史的な論文(旧バージョン関連)
F* の系譜を形作る重要な初期研究です。
| タイトル | コンフェレンス | 概要 |
|---|---|---|
| Value-dependent Types | ICFP 2011 (JFP) | 安全な分散プログラミングへの導入。 |
| 自己認証:Coq で F チェッカーを認証* | POPL 2012 | F* そのものでタイプチェッカーを実装し、Coq で正しさを証明(ブートストラップ)。 |
| JavaScript への完全抽象的コンパイル | POPL 2013 | ML 様な言語から JavaScript へ安全なコンパイラの開発。 |
| 攻撃的文脈における健全性確保 | POPL 2014 | 防御チェック付き JavaScript コンパイラの実装。 |
| 確率的関係検証 (RF)* | POPL 2014 | ゲームベースの暗号証明や非干渉性などの性質の検証。 |