F*（F Star）とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語早わかり

Last updated at 2026-08-02Posted at 2026-08-01

はじめに

皆様が Python でコードを書くとき、そのコードの正しさを保証する手段は、テストを書くこと、そして型ヒントを書くことまでです。

しかし、テストが教えてくれるのは「試した入力については正しく動いた」ことだけです。
テストしていない入力については、何の保証もありません。

F*（F Star）言語を採用すると、事情が違ってきます。

「このコードは、あらゆる入力に対して仕様どおりに動く」ことを、数学的に証明できるようになるのです。

このF*（F Star）言語は研究室の中だけのものではありません。

Mozilla Firefox、Linux カーネル、WireGuard VPN の内部では、F* によって数学的に正しさが証明されたコードが１年365日24時間、稼働し続けているからです。

さらに、AI Agent がコードを書く時代が到来したことで、「生成されたコードの正しさを数学的に保証する」証明指向プログラミングの価値は、急速に高まっています。

ところが、この F*（F Star）を扱った日本語の記事は、ほとんど存在しません。

そこで本記事では、F*（F Star）という言語を、日本語で体系的にご紹介します。

なお、本記事は、F* の文法を解説する記事ではありません。

この記事の目的は、「F*（F Star）が、コンピュータ・サイエンス全体の中で、どこに位置する言語なのか？」
── 関数型・論理型・定理証明・形式検証・依存型・篩型・SMT・エフェクトという文脈の中での F* の位置付け ──
を理解していただくことです。

それでは、始めましょう。

F*（F Star）はプログラミング言語の名前です

F*(F Star) は、プログラミング言語の名前です（読み方は「エフ・スター」）。

定理証明言語（定理証明言語については、この記事の中で解説します）の世界で 1984年以来 40年以上にわたって世界をリードしてきた フランスの国立研究所 INRIA（1967年設立、パリ近郊、定理証明系 Coq(現 Rocq)の生みの親）と、Microsoft Research が、2011年に共同で世に送り出した「証明指向プログラミング言語(proof-oriented programming language)」と呼ばれる 新しいカテゴリの言語 です。

書いたコードそのものに、「あらゆる入力に対して仕様通りに動く」という数学的な証明を、コードの中に書き込むことができます。

皆様が今この瞬間、利用されているかもしれないMozilla Firefox、Linux カーネル、WireGuard VPN、Tezos ブロックチェーン、ElectionGuard 電子投票 SDK、mbedTLS などの実務システムの内部で、F*（F Star）によって数学的に正しさが証明されたコードが稼働していることで、皆様の通信の安全が守られています。

この記事を書く理由：日本語圏における F*（F Star）の記事の少なさ

この記事冒頭で「日本語の記事はほとんどない」とお伝えした状況に目を向けたいと思います。
2026年8月1日正午現在、Qiitaには F*（F Star）タグの記事が３件しかありません。

日本語圏における F*（F Star）の存在感は、F*（F Star）と同じ定理証明・形式証明の領域に属するLean 4やRocq(旧称 Coq)といった言語に関する記事の数と比較すると、とても少ない印象を受けます。

視線をQiita以外のZenn、note、エンジニアやプログラマの皆様の個人ブログ記事や企業の技術ブログ記事に転じても、日本語でF*（F Star）を扱ったウェブサイト・ブログ記事・資料は、本記事執筆者がwebで確認できた範囲では、次のものが見つかるくらいです。

やはり記事の本数の少なさが際立っているという印象を受けます。

F*(F Star)の複雑な型システムの何が嬉しいのか?(はてなブログ、ゆーちき氏、2018年)
F* における検証されたプログラミング(Metasepi プロジェクトによる F* 公式チュートリアルの日本語翻訳)
Metasepi プロジェクト F* 日本語情報サイト
依存型言語 F*のインストール+実行可能コード生成までの手順(2022年)(Zenn、ゆーちき氏、2022年)
F*でプログラムの正しさを証明する(Speaker Deck、Ushitora Anqou 氏、2021年)
F* (プログラミング言語) ── 日本語 Wikipedia
F* (プログラミング言語) ── Weblio 辞書
テストから証明へ ── Z3とLean 4による形式検証の現在地(note、loyal_kalmia8068 氏、2026年、F* に軽く触れているのみ、Lean 4 が主題)

海外の状況： F*（F Star）の個人ブログ・企業技術記事の動静

海外では、F*（F Star）に関するプログラマ・エンジニアの個人ブログ記事や、企業の技術ブログ記事は多いのでしょうか？

F*（F Star）は、世界的に見ても、まだニッチな存在です。

英語圏・中国語圏・韓国語圏・ロシア語圏・インドのいずれにおいても、個人ブログや企業技術ブログでの言及は限られています。

次の節で、各言語圏ごとの状況を掲載しました。
海外の動向に興味をお持ちの方は、ご参考にされてください。

言語の特徴や実装コード例を早く確認されたい方は、次の節を読み飛ばしていただいて構いません。

（英語圏の状況）

英語圏での F(F Star) の情報発信は、学術論文と公式リソースが中心*で、個人ブログや企業技術ブログでの言及は、F#(F Sharp) や他の主要言語と比較すると、決して多くはない、というのが本記事執筆者の観察です。

英語圏の主要な情報源として、本記事執筆者が web で確認できたのはおおむね次の通りです。

F* 公式ブログ（https://fstarlang.github.io/）
── 「F* for the masses」と題された公式ブログ。開発チームによる技術的な投稿が、Dijkstra モナド、パーサ技術、エンジニアリング上の議論といった主題で、定期的に投稿されています
F* Zulip コミュニティ（https://fstar.zulipchat.com）
── 開発者との対話が行われる公式のチャット・プラットフォーム
F* GitHub Discussions
── ユーザーからの質問や議論の場
fstar-club メーリング・リスト
── 公式のアナウンス用リスト（F* 公式サイトの記述によれば「トラフィックはとても少ない」とのこと）
Hacker News での議論
── 2024年6月の "F* – A Proof-Oriented Programming Language" スレッド（https://news.ycombinator.com/item?id=40377685）などがあり、コメントには実務エンジニアが F*(F Star) に関心を持ちつつも、実際の学習・利用にまで踏み込めていない状況が伝わってきます
Medium 等の個人技術ブログ記事
── Volodymyr Pavlyshyn氏の Medium 記事(2025年3月)などが散見されますが、その数は限られています

F* に関する情報は多くの場合、この言語を開発したMicrosoft ResearchやINRIA の学術論文と公式リソースを源流として、そこから派生する形で生まれた技術記事が中心であるという構造が見受けられます。

（中国語圏の状況）

中国語圏では、2024年頃から、F*（F Star）を扱う技術記事が徐々に増えてきています。

本記事執筆者がウェブ上で確認できた主要な例は、次の通りです。

CSDN（中国最大級のプログラマ・コミュニティ）の F* 記事「探秘 FStar:一个高级形式验证的 ML 方言」（2024年3月、blog.csdn.net）
OSCHINA（中国オープンソース技術コミュニティ）の F* ページ（2024年12月、oschina.net）
GitCode 博客の F* チュートリアル「F* 编程语言教程」（2024年9月）
万维易源(showapi.com)の F* 記事「深入探索 F* 编程语言」（2024年10月）

中国語圏の F* 記事数は、本記事執筆者の確認した範囲では、日本語圏と同程度、あるいはやや上回る印象です。

ただし、これらの多くが 2024年後半に集中していることから、中国語圏でも F*（F Star）は近年注目を集め始めたばかりであるという状況が読み取れます。

機械学習や深層学習、LLM・AI Agentでは、国際的なトップ会議に採択された英文論文の本数も、GitHubリポジトリの数もブログ技術記事の数も、中国語（多くは簡体字字。台湾・香港の繁体字ではない）の情報量は、和文（日本語）のそれを遥かに圧倒している状況です。

一例を挙げると、以下のとおりです。

NeurIPS、ICML、ICLR などのトップ会議での中国機関の採択論文数の急増
GitHub での中国発 LLM プロジェクト(Qwen、DeepSeek、GLM、ChatGLM、Baichuan、Yi、Kimi など)の圧倒的存在感
中国語 AI 技術ブログ(CSDN、掘金(Juejin)、知乎、微信公众号)の圧倒的な記事数

そうした状況に比べると、F*（F Star）言語に関しては、日中両言語で書かれたウェブ空間上のブログ記事の数量には、劇的な差はない様子が窺えます。

なお、F*(F Star) 以外の定理証明系 ── Coq(現 Rocq)、Lean 4、Isabelle、Agda など ── については、状況が異なる可能性があります。

本記事執筆者が web で確認した範囲では、次のような事実が浮かびます。

北京大学の北京国际数学研究中心（BICMR）
同数学研究センター（「数学研究中心」）はLean workshops を主催しており、中国国内の Lean を用いた数学の形式化の重要な拠点になっています（Renmin University of China 他の研究者による Lean 用の Premise Retrieval Model 研究 arXiv:2501.13959 の謝辞で確認済）。
上海交通大学（SJTU）の John Hopcroft Center of Computer Science
Coq/Rocq を用いた形式検証(セパレーション論理を用いたC言語プログラム検証ツール QCP、量子言語の意味論の形式化など)の研究の中心の一つで、Qinxiang Cao 氏らの研究チームが継続的に論文を発表しています。
西湖大学（Westlake University、杭州）
中国国家自然科学基金（NSFC Grant No. 12574176）の支援を受けて Lean workshop を開催しており、中国研究者による LeanCat（圏論の形式化ベンチマーク）、FATE（代数のベンチマーク）、REAL-Prover（retrieval augmented Lean prover） といった大規模プロジェクトが、arXiv 上で継続的に発表されています。
華東師範大学（East China Normal University） Shanghai Key Laboratory of Trustworthy Computing
上海交通大学と共同で、Coqを用いた形式検証の研究を行っています。
中国語圏のプラットフォーム（CSDN、知乎、博客园など）
Lean 4 と Mathlib、Coq/Rocq に関する技術記事が、多数蓄積されています。本記事執筆者が確認した主要な例は、次の通りです。
- CSDN の Lean 数学库 mathlib 解説記事「探秘 Lean 数学库 mathlib:构建形式化数学的新里程」(2024年11月、blog.csdn.net)
- 知乎（Zhihu、中国語圏最大規模の知識共有プラットフォーム）の Lean4/Mathlib4 解説記事「Lean4 - Mathlib4 / 用于形式化数学的准备」(2023年、zhuanlan.zhihu.com、Peter Scholze の Perfectoid Spaces の形式化と、Kevin Buzzard の 2022年 ICM 講演に触れながら Lean を紹介)
- 博客园（cnblogs）の Lean 4 学習記事「【学习笔记】Lean4 定理证明 ing」(2025年7月)、「数学证明助手 Lean」(2023年7月)
- 個人ブログの Lean 4 解説記事 ── longfangsong.github.io「定理证明器背后的数学原理」など

F*(F Star) 単体で見ると、日中両言語圏の記事数に劇的な差は見られない印象を受けます。

しかし、視野を他の形式証明・定理証明のメジャーな言語であるLean 4言語と Coq/Rocq言語にまで広げると、中国語圏の情報発信の厚みは日本語圏を上回っている領域が生まれ始めている状況が浮かび上がってきました（2026年8月1日正午現在）。

この状況が意味することは何か

定理証明・形式検証の領域は、世界全体で、いま次の３つの領域で注目を集めています。

数学の形式化（Peter Scholze、Kevin Buzzard、Terence Tao らの潮流）
AI Agent × 定理証明（DeepSeek-Prover、Kimi-Prover、REAL-Prover などの Auto-formalization の潮流）
セキュリティ・クリティカル・ソフトウェアの形式検証

中国は上記の３つの流れすべてに国家的な規模で本格的に参入しています。

【コラム】中国の統治構造と、定理証明・形式検証への国家的関与の輪郭(クリックで展開)

中国の統治構造と国家的関与の輪郭

中国の統治構造を、日本との対応関係で最初に整理します。

中華人民共和国国務院（简: 国务院、英: State Council of the People's Republic of China）
国務院は、中華人民共和国の中央政府・国家行政機関です。国務院は、諸外国における「内閣」に相当します。
この国務院は、国務院総理（首相）が主宰し、副総理、国務委員、各部の部長（大臣に相当）などから構成されます。
国務院総理（首相）
中国共産党中央政治局常務委員から必ず選出されます。中国の統治構造は、「以党領政（党が政府を指導する）」 と表現され、中国共産党中央委員会が党・政府・軍・国家機関全体を指導する立場にあります。つまり、旧ソ連と同様に、党（共産党）が国家・政府（国務院）より上位に位置します。これは社会主義・共産主義国家に共通してみられる統治構造です。（国務院の傘下にある外交部長（外務大臣に相当）よりも、中国共産党中央外事工作委員会 ── その主任は党中央政治局常務委員（現在は習近平国家主席が兼任）、その弁公室主任は党中央政治局委員（現在は王毅氏）── の方が、対外政策の決定においては上位に位置付けられています）
全国人民代表大会（NPC、全人代） は、日本の国会に相当する立法機関ですが、共産党の指導的地位のもとで運営されます。国務院、最高人民法院、最高人民検察院などの構成員を選出する権限を持ちます。

このため、「中国の国家的な関与」 という言葉は、実務的には、「中国共産党中央委員会が方針を決め、国務院とその指揮下の各部・委員会が実施し、国家自然科学基金委員会などの資金機関を通じて具体の研究資金が配分される」という構造を指します。

中国の国家的関与の３つの層

中国政府の関与は、次の３つの層で観察できます。

第１層 ── 政策の枠組み

《"十四五(第14次５カ年計画)"数字経済発展規劃》（2021年-2025年）
── 国務院が発表。AI、量子情報、集積回路、脳科学、深地深海 などを国家戦略の前線領域として位置付け。
《新一代人工智能発展規劃》（2017年、国務院発表）
── AI を国家戦略の中核に位置付けた最初の総合的な文書。
《"十五五"規劃建議》（2025年、中国共産党中央委員会発表）
── 「人工智能+」行動を明記し、基礎理論と核心技術の突破、算力・算法・データの高効率供給を国家目標として設定。
《中共中央国務院印发《拡大内需戦略規劃綱要（2022-2035年）》
── 中国共産党中央委員会と国務院が共同で発表する政策文書は、党と政府の両方の権威を背景に持ちます。

第２層 ── 具体的な国家資金

定理証明・形式検証・数学の形式化・AI Agent × 定理証明の分野における中国政府の資金として、本記事執筆者が arXiv 上の論文の謝辞で確認できた具体例は次の通りです。

国家自然科学基金委員会（National Natural Science Foundation of China、NSFC）
── 中国最大の基礎科学研究資金機関
- NSFC Grant No. 12574176
  ── 西湖大学(Westlake University)における Lean workshop を支援（LeanCat プロジェクト）
- NSFC Grant No. 62276152、62236011、62025202
  ── Autoformalization、Lean を用いた数学の形式化の研究を支援
国家重点研究開発計画（National Key R&D Program of China）
── 国務院・科学技術部が主導する国家重点計画
Grant No. 2024YFA1014000、2024YFA1014001
── Lean を用いた形式化と自動定理証明の研究を支援（FATE ベンチマーク、REAL-Prover、Renmin University of China の Premise Retrieval Model 研究）
Grant No. 2022YFA1008200
── ATLAS（Autoformalizing Theorems）の研究を支援
Grant No. 2023YFC3341203 ── Discover and Prove(Lean 4 用の自動定理証明フレームワーク)を支援
地方政府による資金
上海市科学技術重点プロジェクト（Shanghai Municipal Science and Technology Key Project） No. 22JC1401500、No. 2021SHZDZX0102
北京市自然科学基金（Beijing Natural Science Foundation） Grant No. L233008

第３層 ── 実行主体としての大学・研究機関・民間企業

北京大学北京国際数学研究中心(BICMR) ── Lean workshops を主催
上海交通大学 John Hopcroft 計算機科学中心 ── Coq/Rocq を用いた形式検証（Qinxiang Cao 氏）
華東師範大学上海市可信計算重点実験室 ── Coq を用いた量子言語の意味論の形式化
西湖大学(Westlake University、杭州) ── NSFC の支援のもとでの Lean workshop
人民大学(Renmin University of China) ── Lean の Premise Retrieval Model 研究
DeepSeek AI ── DeepSeek-Prover シリーズ（Lean 4 を用いた自動定理証明の大規模言語モデル）
Moonshot AI ── Kimi-Prover / Kimi K2 / Kimina Lean Server（Lean を用いた自動定理証明の高性能サーバー）
StepFun AI ── StepFun-Prover(段階的推論による定理証明)

３つの流れごとに、中国の国家的関与の姿

数学の形式化への関与

中国の主要大学（北京大学、上海交通大学、西湖大学、人民大学など）
Lean 4 と Mathlib を用いた数学の形式化研究が、NSFC・国家重点研究開発計画の資金を得て、継続的に arXiv・国際会議に発表されています。
Peter Scholze、Kevin Buzzard、Terence Tao らの潮流に、中国の研究者（Bin Dong 氏、Xiaoxing Ma 氏、Qinxiang Cao氏他）が国家資金の後押しを受けて参加している構造が観察できます。

AI Agent × 定理証明への関与

DeepSeek-Prover、Kimi-Prover、REAL-Prover、StepFun-Prover、LeanMarathon など、Lean 4 を用いた自動定理証明の大規模言語モデルが、2024-2026 年にかけて中国発で相次いで発表されました。

これらは、《"十四五"数字経済発展規劃》 および 《新一代人工智能発展規劃》 で位置付けられた「AI 基礎理論の突破」に沿う成果であり、中国政府の政策と、DeepSeek、Moonshot、StepFun などの民間 AI 企業の投資が呼応する形で進展しています。

中国発の DeepSeek-Proverと日本の東京大学発の Prover Agent(2025年、arXiv:2506.19923)、韓国発の研究など、東アジア圏の Auto-formalization 研究の中で、中国は資金規模と論文数の両方で先頭集団にいます。

セキュリティ・クリティカル・ソフトウェアの形式検証への関与

上海交通大学 John Hopcroft 中心と華東師範大学上海市可信計算重点実験室（Shanghai Key Laboratory of Trustworthy Computing）
Coq/Rocq を用いた C言語プログラムの形式検証、量子言語の意味論の形式化を継続しています。
Shanghai Key Laboratory of Trustworthy Computing の名称に「可信計算（Trustworthy Computing、信頼できる計算）」が明示的に含まれていることは、中国政府がセキュリティ・クリティカル・ソフトウェアの形式検証を、重要な戦略分野として位置付けていることを示しています。

全体を俯瞰すると

中国は、政策の枠組み（国務院・党）、具体的な国家資金（NSFC・国家重点研究開発計画）、実行主体（大学・研究機関・民間AI企業）の３つの層で、定理証明・形式検証の分野に、国家的な規模で本格的に参入していると考えられます。

この技術領域は中国にとって、「AI 基礎理論の突破」「Trustworthy Computing」という２つの国家戦略のクロス地点に位置し、今後さらに投資が拡大する可能性が高いと受け止めることができます。

日本語圏の技術者の皆様が、この分野で情報発信をなさることは、単に「日本語圏の空白を埋める」以上の意味 ── 世界の主要言語圏の一つとして、この学問領域の発展に加わることにつながります。

韓国語圏、ロシア語圏、インド発の個人ブログの状況

韓国語、ロシア語、インドの各言語や英語での、F*（F Star）を主題とする個人ブログ・企業技術記事は、本記事執筆者がwebで確認できた範囲では見つかりませんでした。

これは、これらの国で F*（F Star）がまったく扱われていないという意味ではなく、これらの国々では、 F*（F Star）の情報発信が大学の研究室内・企業の内部ドキュメント・学術論文といったwebで検索されにくい場所に留まっている可能性が考えられます。

全体を俯瞰すると

F*（F Star）は、2026年8月1日時点では、世界のどの言語圏においても、まだ「エンジニアの間で広く記事が書かれる主流言語」の地位を獲得するには至っておらず、「学術研究と実務領域の狭間で、専門的なコミュニティに支えられて発展する言語」の位置に留まっている、というのが本記事執筆者の状況評価です。

この事実は、日本語圏の皆様にとって、２つの意味を持ちます。

まず第１に、どの言語圏でも F*（F Star）の情報がまだ少ないということは、日本語圏で F*（F Star）を扱う皆様が、世界でも最初期の実務者・書き手・翻訳者の一人になれる可能性があります

第２に、日本語での学習資料の少なさは、皆様がF*（F Star）言語を学ばれる際の障壁**でもあります。この記事が、その障壁を少しでも下げる一助になりましたら幸いです。

言語の名称表記について

なお、言語の名称の表記について触れておきます。

英語コミュニティにおける表記は、「F*」「F star」「F Star」の3つが主に使われています。

日本語圏での表記は、「F*」「F*（F Star）」「F*（F スター）」といった書き方が使われています。

この記事では、想定読者の皆様に読みやすい形として、F*（F Star） の表記を採用します。

これまでプログラミング言語は Python だけを使われてきたエンジニアの皆様に、F*（F Star）とは何か、どんな立ち位置にある言語で、どんな経緯で生まれ、どんな用途があり、今から学ぶ価値があるのかを、ワンストップでお伝えします。

F*（F Star）とはどんなプログラミング言語か

F*（F Star）は、プログラミング言語の名前です(読み方は「エフ・スター」)。Microsoft Research と INRIA(フランス国立情報学自動制御研究所)が 2011年に共同で世に送り出した、「証明指向プログラミング言語(proof-oriented programming language)」と呼ばれる新しいカテゴリの言語です。

皆様が書いたコードの中に、「あらゆる入力に対して仕様通りに動く」という数学的な証明を書き込むことができます。

F*（F Star）言語がこうした仕組みを備えていることで、開発者は「テストで一つ一つの入力を確かめる」のではなく、「あらゆる入力に対する正しさを一度に数学的に保証する」というレベルの厳密さを社会システムを支える実装コードに付与することができます。

F*（F Star）の一次情報源

F*（F Star）についての一次情報は、以下の場所で公開されています。

公式サイト
https://fstar-lang.org
GitHub 公式リポジトリ
https://github.com/FStarLang/FStar
公式ブログ
https://fstarlang.github.io/
Microsoft Research の F プロジェクトページ*https://www.microsoft.com/en-us/research/project/the-f-project/
Project Everest 公式サイト(F* を用いた主要な応用プロジェクト) https://project-everest.github.io/
F* 公式チュートリアル(英語)
https://fstar-lang.org/tutorial/
F* 公式書籍「Proof-Oriented Programming in F*」(PDF、Nikhil Swamy、Guido Martínez、Aseem Rastogi 著、2024年)
https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf
F* Wikipedia(英語版) https://en.wikipedia.org/wiki/F*_(programming_language)
F* Wikipedia(日本語版) https://ja.wikipedia.org/wiki/F*_(%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0%E8%A8%80%E8%AA%9E)
F* Wikidata
https://www.wikidata.org/wiki/Q5423569
主要学術論文
- ICFP 2011論文「Secure Distributed Programming with Value-Dependent Types」(Nikhil Swamy 他、F* の初代設計の基準論文)
- POPL 2016論文「Dependent Types and Multi-Monadic Effects in F」*(Nikhil Swamy 他、現代の F*の設計を確立した基準論文)

上記のすべての一次情報源で、この言語は「F*」(F と半角アスタリスク)という表記で紹介されています。

読み方は「エフ・スター」で、英語では「F star」または「F Star」とも書かれます。

この記事でも、以降は基本的に F*（半角アスタリスク）の表記を使い、必要な箇所で F*（F Star） と併記する形で、皆様の読みやすさを保ちます。

F*（F Star）と名前が似ている F#（F Sharp）との区別

F*（F Star）は、名前が似ている F#（F Sharp）とは異なるプログラミング言語です。

皆様の中には、Visual Studio に付属する言語の一つとして、あるいは.NET プラットフォームの関数型言語として、F#（F Sharp）の名前を目にした皆様もいらっしゃるかもしれません。

F#（F Sharp）
── Don Syme が Microsoft Research Cambridge で主導し、2005年に世に出た関数型プログラミング言語です。.NET プラットフォームで動作し、OCaml から強く影響を受けています。
開発の目的は「関数型プログラミングを .NET プラットフォームで実用的に使えるようにする」ことでした。
F*（F Star）
── 2011年に、Nikhil Swamy 他が Microsoft Research と INRIA の共同開発として世に出した証明指向プログラミング言語です。

なお、F*（F Star）言語は、F#言語から影響を受けています（F* を書いたコードは、F# のコードに翻訳して実行することもできます）。

しかし、F*（F Star）の目的は、F#（F Sharp）とは根本的に異なります。

F*（F Star）の目的は、「書いたコードそのものの正しさを、数学的な証明として、コードの中に書き込めるようにする」ことです。

両者は「名前が似た、別の言語」であり、この記事では証明指向プログラミング言語 F*（F Star）の側を主題として扱います。

両者の違いを表に整理しました。

	F#（F Sharp）	*F（F Star）**
目的	関数型プログラミングを .NET で実用化	証明付きプログラム(証明指向プログラミング)
主な用途	一般のアプリケーション開発	セキュリティ・クリティカルな領域の形式検証
登場年	2005年	2011年
開発主体	Microsoft Research Cambridge(Don Syme 氏が主導)	Microsoft Research と INRIA の共同開発

「F」というアルファベット一文字が名前の一部に使われているプログラミング言語は、他にも以下があります。

Fortran
1957年、IBM が開発、科学技術計算の先駆的な言語
Forth
1970年、Charles Moore が開発、スタック指向の言語
Factor

など、複数存在します。

この記事で扱う F*（F Star）は、これらの言語群の中で「証明指向プログラミング」という極めて特殊な目的**を持つ、希少な位置を占める言語です。

想定読者

これまでプログラミング言語は Python だけを使われてきたエンジニアの皆様
形式証明・定理証明・依存型プログラミング・関数型プログラミング・論理型プログラミングについて、これまで学ぶ機会がまだなかった皆様
F* という言語の名前は聞いたことがあるが、これまで詳しく触れる機会がなかった皆様
証明指向プログラミングという言葉を、これまで聞く機会がなかった皆様
AI Agent が生成するコードの正しさをどう保証するかに関心のある皆様

前提知識は必要ありません。

8つの概念（関数型、論理型、定理証明、形式検証、依存型、篩型、SMT ソルバー、エフェクト）は、この記事の中で丁寧に解説します。

この記事を読む価値

F* の言語仕様と実行例、そしてその立ち位置が、これまで Python を使ってきた皆様の目線で分かるようになります
依存型と篩型のハイブリッドという表現の意味が、腑に落ちるようになります
関数型・論理型・定理証明・形式検証・依存型・篩型・SMT ソルバー・エフェクトというF* を支える8つの基礎概念の全体像を体系的につかめるようになります
F* が生まれた経緯 ── INRIA と Microsoft の共同研究の歴史と、その目的が分かります
F* が実務で動いている実例（Firefox、Linux、WireGuard、Tezosほか） の全体像が掴めます
AI Agent 時代における F* の学習価値を理解することができます

TL;DR

F* は「証明指向プログラミング言語（proof-oriented programming language）」。
皆様がお使いの言語(Python、Java、Go など)で書けるプログラムを書けるだけでなく、そのプログラムが仕様通りに動くことを、コードの中に証明として書き下ろすことができる言語です。

F* の型システムには、依存型（dependent types）、モナディック・エフェクト（monadic effects）、篩型（refinement types）の３つが備わっています。
この組み合わせは、極めて希少です。

F* は、Microsoft Research と INRIA（フランス国立情報学自動制御研究所）の共同開発で、2011年に登場しました。
開発の動機は、「対話的定理証明系（強い保証だが実用性に限界）と、副作用や並行性を扱う汎用プログラミング言語の間のギャップを埋める」こと でした。

F* の主要な用途は、Project Everest という Microsoft Research 中心の大規模プロジェクトです。検証済みHTTPS スタックを F* で構築し、その成果は Mozilla Firefox、Linux カーネル、Tezos、ElectionGuard、WireGuard VPN、mbedTLS などで実用として動いています。
AI Agent 時代における F* の学習価値は、極めて高いと考えられます。
F* の GitHub 公式リポジトリには、Claude Code や GitHub Copilot CLI からのF* 使用を支援する proof-copilot プラグインが推奨されており、AI Agent が生成するコードの正しさを厳密に検証する場面で、F* は独特の強さを発揮します。

F*（F Star）はどんな言語で、どんな立ち位置を築いているのか

８つの概念を整理する

F* の立ち位置を掴むために、まず８つの概念を順に整理します。

皆様のこれまでのお仕事の場面で、これらの概念に触れる機会が少なかった可能性もありますので、丁寧に解説します。

**１. 関数型プログラミング（ functional programming ）**

関数型プログラミングとは、プログラムを「値を受け取り、値を返す関数」の組み合わせとして書くプログラミング・スタイルです。

Python でも部分的に採用されていますが（map、filter、lambda など）、関数型プログラミングを言語の中心に据えた言語として、Haskell、OCaml、F#、Scala、Elm などがあります。

Pythonとの違いを一言で言えば、関数型プログラミングでは「変数の値を書き換える」ことを避けるという点です。

Python ならx = 5と書いた後でx = 6と書き換えられますが、関数型プログラミングでは、そういう「破壊的な代入」を最小限に抑えます。

この設計により、プログラムの動作が予測しやすくなり、バグが少なくなるという利点があります。

関数型プログラミングの雰囲気を、F*(F Star) のコード実例で見てみましょう。リストの合計を計算する関数を、Python と F*(F Star) の両方で書き比べます。

Python のコード ：

def sum(lst):
    total = 0
    for x in lst:
        total += x
    return total

result = sum([1, 2, 3])  # 6

F*（F Star）のコード :

val sum : list int -> Tot int
let rec sum lst =
  match lst with
  | [] -> 0
  | x :: rest -> x + sum rest

let result = sum [1; 2; 3]  // 6

F*（F Star）の方は、for ループも代入もありません。

「空リストの合計は 0」「先頭 x と残りのリスト rest からなるリストの合計は、x + rest の合計」 という、リストの構造そのままに再帰で書き下ろす形です。

Tot は、「必ず停止し、副作用のない純粋関数」を意味するエフェクト です。

**２. 論理型プログラミング（ logic programming ）**

論理型プログラミングとは、「解きたい問題を、論理的な事実と規則の集まりとして書き、コンピュータに解を探させる」 プログラミング・スタイルです。

代表的な言語は Prolog です。

例えば、「太郎の父親は次郎、次郎の父親は三郎」という事実と、「祖父とは、父親の父親のことである」という規則を書くと、Prolog は「太郎の祖父は誰か」を自動的に導出してくれます。

これまで論理型プログラミングに触れる機会が少なかった皆様もいらっしゃると思いますが、論理型プログラミングは、AI や自然言語処理、データベースの問い合わせなどの分野で、独特の力を発揮します。

**3. 定理証明（ theorem proving ）**

定理証明とは、数学的な命題（定理）を、機械の助けを借りて厳密に証明する営みです。

使う道具として、定理証明系（ proof assistant 、あるいは interactive theorem prover ） と呼ばれる専用のソフトウェアがあります。

代表的なものに、Rocq（旧称 Coq）、Lean 4、Isabelle、Agda などがあります。

定理証明系 は、単にプログラミング言語ではなく、数学の定理を、機械が理解できる形式で書き下ろし、その証明を機械が一つ一つ確認するためのシステムです。

四色定理や、Kepler 予想、プログラム言語の型安全性など、数学とコンピュータサイエンスの重要な結果が、定理証明系で厳密に検証されています。

この点は、以前公開しました定理証明・形式検証はいまから学ぶ価値があるか ── なぜ「人が仕様を書く」必要があるのか、Lean 4 から始める学習ロードマップにも詳しく書いていますので、興味のある皆様はご参照ください。

**4. 形式検証（ formal verification ）**

形式検証とは、プログラムが仕様通りに動くことを、あらゆる入力に対して数学的に証明する営みです。

定理証明の技術を、ソフトウェア開発に応用したもの と言えます。

Pythonを使用する場合、皆様は「テストコードを書いて、いくつかの入力について動作を確かめる」という方法を取るでしょう。

しかし、テストは有限個の入力しか確かめられません。
10万個の入力についてテストが通っても、100万個目の入力で失敗する可能性は残ります。

形式検証は、この根本的な限界を超えます。

「あらゆる入力について、このプログラムは正しく動く」ことを、数学的な証明として書き下ろし、機械にその証明を検査させるのです。

この保証の強さは、テストとは根本的に違います。

**5. 依存型プログラミング（ dependent type programming ）**

依存型プログラミングとは、値の性質を型の中に書き込むプログラミング・スタイルです。

Pythonであれば、プログラマはx: intと書くだけで、「x は整数である」ことを表現できます。

しかし、「x は正の整数である」「x は5より大きい整数である」「x は素数である」といった、値のより詳しい性質を、型として書くことはできません。

依存型プログラミング言語では、こうした「値の性質」を、型そのものとして表現し、コードに記述することができます。

例えば、Vector Int 3と書けば、「長さがちょうど3の整数のベクトル」を意味する型として、その意味を型が保持 します。

代表的な依存型言語には、Idris、Agda、Lean 4、Rocq、そして F*（F Star） があります。

**6. 篩型（ refinement types ）**

篩型は、依存型と近い技術で、型に、値が満たすべき論理的な条件（述語）を書き加えることで、値の性質を表現します。

例えば、x:int{x > 0}という型は、「x > 0を満たす整数x」を意味します。

依存型と篩型の関係については、以前公開しましたPythonの型ヒントの限界を超える「篩型」入門 ―― "x > 0" を型に書くと何が起きるのか（LiquidHaskell・F*・Typed Racket・Idris 2 への誘い）に詳しく書いています。

F*（F Star）の型システムは、依存型と篩型の両方を統合しています。
この点は後の節で詳しく扱います。

**7. SMT ソルバー（ SMT Solver 、Z3 ）**

SMT（ Satisfiability Modulo Theories、理論付き充足可能性） は、「与えられた論理式を成り立たせるような変数の値の組み合わせが、存在するかどうか」を、機械的に判定する技術です。

例えば、「$x > 0$ かつ $x < 10$ かつ $x は偶数$」という条件を与えると、SMTソルバーは、「$x = 2$ なら成り立つ」と自動的に見つけ出してくれます。

SMTソルバーは、この判定を行うソフトウェア です。

もう少し具体的に言えば、SMTソルバー は、整数、実数、配列、ビットベクトルなどの数学的な性質を組み込んだ上で、複雑な論理式の真偽を、極めて高速に判定します。

例えば、「$x が 10 より大きく、かつ x - 11 が 0 になる、そんな整数 x はあるか$」という問いに対して、SMTソルバーは、「あります。$x = 11$ です」と答えます。

代表的なSMTソルバーは、Microsoft Researchが開発したZ3 です。

F*（F Star）は、この Z3 を標準の証明エンジンとして統合しており、書き手が明示的に証明を書かなくても、Z3が自動的に多くの証明を機械的に判定してくれます。

この特徴が、F*（F Star）の実用性の大きな源泉です。

SMTソルバーの力を、F*（F Star）のコードの実例を通して見てみましょう。

例題は、ゼロ除算を、コンパイル時に型で防ぐ関数です。

val safe_div : x:int -> y:int{y <> 0} -> Tot int
let safe_div x y = x / y

// 呼び出し例
let result1 = safe_div 10 2   // OK、5 が返る
// let result2 = safe_div 10 0   // コンパイル・エラー(型が y <> 0 を要求)

引数 y の型に int{y <> 0} と書き加えるだけで、「$yは0ではない整数$」という条件が、型として表現されます。

F*（F Star）のコンパイラは、Z3を裏で呼び出し、呼び出し側で$y$に$0$が渡される可能性を機械的に判定します。

もしも$0$が渡される可能性があれば、コンパイル時にエラーで拒否されます。

Python なら、実行時に「ZeroDivisionError」が発生しますが、F*(F Star) では、プログラムを走らせる前の段階（コンパイル時）にゼロ除算の可能性を Z3 が捕捉してくれます。

**8. エフェクト（ monadic effects 、モナディック・エフェクト）**

エフェクトとは、関数の副作用を、型で追跡する仕組みです。

Python なら、def f(x): print(x); return x + 1のような関数は、「printで画面に出力する」という副作用を持ちます。

しかし、Pythonの型ヒントでは、この副作用を型として表現することはできません。

関数型プログラミング言語の一部（特に Haskell、F*（F Star）、Idris など）は、「この関数はこういう副作用を持つ」ことを型として表現（記述）することができます。

この仕組みのことを、モナディック・エフェクト と呼びます。

F*（F Star）は、以下に示す複数のエフェクトを、型として記述することが可能です。

Tot(Total、トータル、「必ず終わる」の意)
純粋で必ず停止する関数(副作用なし、無限ループなし)
ML(Meta Language、メタ・ランゲージ、OCaml や F# などの ML 系言語の名前) 副作用のある可能性がある関数(OCaml の関数と同じような自由度)
ST(State、ステート、「状態」の意)
状態(参照)の読み書きを行う関数
Exn(Exception、エクセプション、「例外」の意)
例外を発生させる可能性がある関数
Dv(Divergence、ダイバージェンス、「発散」の意、無限ループを含む場合の呼称) 無限ループする可能性がある関数

この仕組みを備えているF（F Star）言語は、「この関数は副作用を持たない」「この関数は状態を変更する」といった性質を、型として明示的に記述する能力を持ちます*。

そして、F*(F Star) のコンパイラは、その型と実装が一致しているかを（実行時ではなく、コンパイラ時に）機械的に検査してくれるのです。

上記５つのエフェクトそれぞれについて、F*（F Star）のコードを通して見ていきましょう。

Tot：純粋で必ず停止する関数

val add : int -> int -> Tot int
let add x y = x + y

let result = add 3 5  // 8 が返る

副作用がなく、必ず有限回で計算が終わる関数は、Totエフェクト を持ちます。
同じ引数を渡せば、必ず同じ結果が返ります。

この「副作用がなく、必ず停止し、同じ入力には必ず同じ結果を返す」という最も強い保証は、計算の核心部そのものを担う領域で威力を発揮します。

暗号アルゴリズムの計算核心部 ── 暗号化・復号・ハッシュ計算といった処理は、「同じ鍵と同じ入力からは、必ず同じ結果が出る」ことが大前提の純粋な計算のかたまりです。
HACL* の暗号関数群の核心部が強い保証の下で書かれているのは、まさにこの性質のためです。
暗号計算が「たまに違う結果を返す」「まれに終わらない」ことは、絶対に許されません。
証明の部品としての利用 ── ここが Tot の最も重要な役割です。
F*（F Star）では、証明の中で使える関数は原則として Tot でなければなりません。
なぜなら、無限ループするかもしれない関数や、実行のたびに結果が変わる関数を証明の根拠にすると、論理の土台そのものが崩れるからです。
Totは、「証明の世界に持ち込んでよい、信頼できる計算」の資格証明なのです。
パーサ・データ変換の核心ロジック ── 「必ず停止する」という保証は、どんな入力を与えられても処理が固まらないことを意味します。
悪意ある入力でパーサを無限ループに陥らせるサービス拒否（DoS）攻撃は実在する脅威であり、停止性が型で保証されていれば、この種の攻撃の可能性を実行前に排除できます。

テスト不能なほど入力空間が広い計算 ── 「同じ入力なら必ず同じ結果」（参照透過性）が保証された関数は、動作が入力だけで決まるため、数学的な証明の対象にしやすくなります。
テストでは到底カバーできない広大な入力空間を持つ計算ほど、Tot として書いて証明を付ける価値が大きくなります。

５つのエフェクトの中で、Tot は最も制約が強く、その代わり最も強い保証を与えます。

F*（F Star）の証明の体系全体が、この「必ず終わり、必ず同じ答えを返す」関数たちを土台として組み上げられているのです。

ML：副作用のある可能性がある関数

val print_and_add : int -> int -> ML int
let print_and_add x y =
  FStar.IO.print_string "計算中\n";
  x + y

let result = print_and_add 3 5  // 画面に「計算中」と表示し、8 を返す

画面出力やファイル読み書き、乱数生成といった副作用を伴う可能性がある関数は、MLエフェクト を持ちます。

OCamlと同じくらい自由に副作用を書けるエフェクトです。

ML エフェクトの価値は、他のエフェクトとは少し性格が異なります。

「副作用を細かく制限する」のではなく、「ここから先は OCaml 並みの自由さで書く」と型で宣言できること ── つまり、証明の世界と実用の世界の境界線を引けることが、ML エフェクトの威力です。

「OCaml 並みの自由さ」について、補足します。

関数型プログラミング言語と聞くと、「変数の書き換えを避ける」「副作用を抑える」といった制約の多い世界を想像されるかもしれません。実際、Haskell のような言語では、画面出力ひとつにも特別な作法が求められます。

しかし OCaml は、関数型言語でありながら、「必要なら普通に書いてよい」という現実路線を採る言語です。画面に文字を表示する、ファイルを読み書きする、変数の値を書き換える ── こうしたことを、Python とほぼ同じ感覚で、特別な作法なしに書くことができます。

つまり「OCaml 並みの自由さ」とは、「Python でいつも書いているような、画面出力もファイル操作も混ざったコードを、そのままの感覚で書ける」 という意味です。

MLエフェクトを持つ関数の中では、証明のための特別な制約を意識する必要はありません。

入出力を伴う「外側」の処理 ── 画面表示、ログ出力、ファイル読み書き、コマンドライン引数の処理といった、プログラムと外界との接点は、数学的な証明の対象にしにくい部分です。こうした部分を ML エフェクトとして書くことで、「証明すべき核心部（Tot や ST）」と「自由に書いてよい周辺部（ML）」を、型のレベルで明確に分離できます。
検証済みライブラリを駆動するアプリケーション本体 ── HACL* のような検証済み暗号ライブラリを実務で使うとき、暗号処理の核心は証明済みのコードが担い、それを呼び出すメイン処理・設定読み込み・結果の出力は ML エフェクトで書く、という役割分担が自然に成立します。「保証の濃い部分」と「普通に書く部分」が混ざらないことが、コード全体の信頼性の見通しを良くします。
プロトタイピングと段階的な検証 ── 最初はすべて ML エフェクトで OCaml のように自由に書き、動くものを作ってから、核心部分だけを段階的に Tot や ST に「格上げ」して証明を付けていく、という開発の進め方ができます。いきなり全体を証明しようとして挫折するのではなく、証明の投資先を選べるわけです。
テストコード・実験コード ── 検証対象の関数を試しに動かすテストドライバや実験用スクリプトは、証明を付ける必要のない典型例です。ML エフェクトがあることで、同じ F*（F Star）のコードベースの中に、証明済みコードとテストコードを同居させられます。

「すべてを証明しなければならない言語」は、実務では使えません。

MLエフェクトは、F*（F Star）に「証明しない自由」を持ち込むことで、証明の厳密さと開発の現実性を両立させる安全弁の役割を果たしているのです。

ST：状態（参照）の読み書きを行う関数

open FStar.ST

val increment : ref int -> ST unit
  (requires fun _ -> True)
  (ensures fun h0 _ h1 -> sel h1 counter = sel h0 counter + 1)
let increment counter =
  let current = !counter in
  counter := current + 1

// 呼び出し例
let counter = alloc 0
let () = increment counter  // counter の値が 0 から 1 になる

メモリ上の参照（ref）を読んだり書いたりする関数は、STエフェクト を持ちます。

関数の型に、状態の変化の仕様（$１$だけ増える）まで書き加えることができる能力が、F*（F Star）の力のひとつ なのです。

この「状態の変化の仕様を型で保証できる」という特質は、状態の管理を誤ると重大な障害や脆弱性に直結する領域で、大きな効果を発揮します。

通信プロトコルの実装 ── TLS のハンドシェイクのような通信プロトコルは、「今どの段階にいるか」という状態遷移のかたまりです。「鍵交換が完了する前に、暗号化データを送ってはならない」といった状態に関する約束事を型として書き込み、その約束が守られていることをコンパイル時に検査できます。miTLS-fstar による TLS 1.3 の検証済み実装は、まさにこの力の上に成り立っています。
OS・システムソフトウェア ── カーネルやデバイス・ドライバは、メモリ上の状態を直接読み書きするプログラムの代表格です。「この関数は、この領域以外のメモリを書き換えない」「解放済みのメモリには決して触れない」といった性質を型として保証できることは、バッファ・オーバーフローや解放後使用（use-after-free）といった、OS の脆弱性の定番を、実行前に締め出すことを意味します。
暗号ライブラリの実装 ── 暗号処理は、内部状態（鍵、カウンタ、中間値）の更新の連続です。HACL* が「メモリ安全であること」まで含めて証明された C コードを生成できるのは、状態の読み書きを型で追跡するこの仕組みが土台にあるからです。
並行処理・カウンタや残高の管理 ── 「口座残高は負にならない」「カウンタは単調に増加する」といった不変条件（invariant）を型として宣言しておけば、その条件を破りうるコードは、そもそもコンパイルを通りません。

「状態を持つプログラム」こそ、バグの温床です。その状態の振る舞いに数学的な保証を与えられることが、F*（F Star）が通信・OS・暗号といったセキュリティ・クリティカルな領域で選ばれている理由の核心にあります。

Exn：例外を発生させる可能性がある関数

exception DivByZero

val divide : int -> int -> Exn int
let divide x y =
  if y = 0 then raise DivByZero
  else x / y

// 呼び出し例
let result1 = divide 10 2   // 5 が返る
let result2 = divide 10 0   // DivByZero 例外が発生

特定の条件下で例外を発生させる可能性がある関数は、Exnエフェクト を持ちます。

Python の raise と同じ発想ですが、「この関数は例外を投げる可能性がある」ことが、型のレベルで宣言される 点が異なります。

この「例外の可能性が型のレベルで宣言される」という特質は、例外の見落としが重大な結果につながる領域で、大きな効果を発揮します。

パーサ・入力検証 ── ネットワークから届くデータや、ユーザーが与えるファイルは、「壊れているかもしれない入力」の代表格です。
Python では、パース関数がどんな例外を投げうるかはドキュメントを読むか実行して初めて分かりますが、F*（F Star）では、「この関数は不正な入力に対して例外を投げうる」ことが型に現れる ため、呼び出し側は例外処理を書き忘れたままコンパイルを通すことができません。
悪意ある入力への対処漏れを、実行前に締め出すことが可能となります。

暗号処理・認証 ── 「署名の検証に失敗した」「復号に失敗した」という失敗は、握りつぶすと即座にセキュリティ・ホールになる失敗です。
失敗の可能性が型として宣言されていれば、「検証失敗を無視して処理を続行する」コードは型検査の段階で拒否することができます。

資源の確保と解放 ── ファイル、ソケット、ロックなどの資源を扱うコードでは、「途中で例外が起きたときに、資源が解放されないまま残る」というバグが定番です。
どの関数が例外を投げうるかが型で見えていれば、解放処理が必要な箇所を、機械的に特定することができます。

金融・決済処理 ── 「送金の途中で失敗したら、必ず全体を取り消す」といった処理では、失敗しうる箇所の見落としがそのまま金額の不整合につながります。
例外の可能性が型に現れることで、失敗経路の網羅をコンパイラが強制してくれます。

Python の例外は「投げっぱなし」にでき、呼び出し側が捕捉を忘れても誰も警告してくれません。
Exnエフェクトは、この**「忘れられる自由」を型の力で取り上げることで、失敗が許されない領域のコードに、「すべての失敗経路が考慮済みである」という保証**を与えるのです。

Dv：無限ループする可能性がある関数

val forever : unit -> Dv unit
let rec forever () = forever ()

// 呼び出し例(この関数は永遠に返らない)
// let () = forever ()

再帰の停止性を証明できない関数、あるいは意図的に無限ループする関数は、Dvエフェクト を持ちます。

Tot が「必ず停止する」保証を要求するのに対し、Dv は「停止しないかもしれない」ことを型で明示します。

停止性の証明の負担を後回しにしたい場面で、Dv を使うことがあります。

この「停止しないかもしれないことを、型で正直に申告する」という特質は、次のようなユースケースで威力を発揮します。

サーバー・イベントループ ── 「停止しないことが正しい」プログラム ── Web サーバーの受付ループ、OS のスケジューラ、ゲームのメインループは、そもそも停止しないことが仕様のプログラムです。
「必ず停止する」ことを求める Tot では、こうしたプログラムはそもそも書けません。
Dv があることで、「意図して回り続けるループ」を、F*（F Star）の型の体系の中に正当な市民として迎え入れることができます。

停止性の証明が本質的に難しいアルゴリズム ── 例えば Collatz 予想（どんな正の整数から始めても 1 に到達するか）に関わる計算のように、停止するかどうかが数学の未解決問題そのものである関数が存在します。また、複雑な再帰では、停止することは経験的に明らかでも、その証明を書き下ろすのが極めて骨の折れる場合があります。
Dv は、こうした関数を「停止性は未証明」と明示した上で書くことを許します。

段階的な開発 ── まず動かし、証明は後から ── 開発の初期には、アルゴリズムの形を試行錯誤する段階があります。
Dv で書き始めれば、停止性の証明を書く前に、まずコードの設計を固めることができます。
設計が固まった後に、停止性の根拠（減少する量、well-founded な順序）を付けて Tot に「格上げ」する ── ML エフェクトの節でご紹介した「段階的な検証」と同じ思想が、停止性についても成り立つのです。

証明の体系を守る防壁として ── ここが Dv の最も重要な役割です。
Tot の節で述べたとおり、停止しないかもしれない関数を証明の根拠に使うと、論理の土台が崩れます。
Dv という「隔離された身分」があるからこそ、停止性未証明の関数が証明の世界に紛れ込むことを型システムが構造的に防いでくれるのです。
Dv は逃げ道であると同時に、証明の純度を守る防疫線でもあります。

「停止しないかもしれない」と正直に名乗らせること ── それが Dv の本質です。

保証を弱めているのではなく、保証の及ぶ範囲と及ばない範囲の境界線を、型の上に明示しているのです。

この正直さがあるからこそ、F*（F Star）は現実のプログラム（回り続けるサーバーも、証明の難しい再帰も）を排除せずに、証明の体系の健全性を保つことができるのです。

以上見てきた5つのエフェクトを比べると、副作用の性質が型で一目で区別できることが分かります。

Python では、関数を外から見ただけでは ── つまり関数の名前や型ヒントを見ただけでは ── その関数に副作用があるのか、必ず停止するのかが分かりません。

中身のコードを一行ずつ読んで、確かめるしかないのです。

F*（F Star）では、この曖昧さが型で解消されます。
型を見るだけで、中身を読まなくても分かるのです。

F*（F Star）の立ち位置

以上の８つの概念に関して、F*（F Star）はどこに位置するのでしょうか。

F*(F Star) は、関数型プログラミング言語であり、依存型プログラミング言語であり、篩型プログラミング言語であり、形式検証の道具であり、定理証明の道具でもある、という複数の性格を併せ持つ極めて希少な言語です。

より正確に言えば、F*（F Star）は次のように位置付けられます。

F*（F Star）は、ML（Meta Language）系の関数型プログラミング言語（OCaml、F#、Standard ML と同じ系統）
F*（F Star）は、依存型と篩型の両方を型システムに備えた、証明指向プログラミング言語
F*（F Star）は、SMT ソルバー（Z3）による証明の自動化と、対話的な定理証明の両方を提供する
F*（F Star）は、モナディック・エフェクトによって、副作用のある関数の性質を型で追跡できる
F*（F Star）は、実用のプログラムを書ける汎用言語でもあり、OCaml、F#、C、WebAssembly、アセンブリ言語などに翻訳できる

この最後の点が、F*（F Star）が持つ特徴の中でも、とりわけ重要と考えられます。

F*（F Star）で書かれたコードは、C 言語、OCaml、F#、WebAssembly、アセンブリ言語などに翻訳して、実用のシステムで動くコードとして動作するからです。

この点では、Microsoft Research 発の Lean 4 も、汎用プログラミング言語として設計されており、C コードにコンパイルして本番環境で動作させることができます。

（この点、Lean 4 と F*（F Star）は、Rocq(旧 Coq)、Agda、Isabelle などの、主に証明の記述に特化した定理証明系とは異なります。Rocq や Isabelle で書いたコードを本番システムで動かすには、OCaml や Haskell への抽出(extraction)を経る必要があります）

F*（F Star）とLean 4は、どちらもC言語のコードに翻訳することができますが、使われる領域が異なります。

F*（F Star）は、Project Everest という Microsoft Research 中心の大規模プロジェクトによって、Mozilla Firefox、Linux カーネル、Tezos、WireGuard、ElectionGuard、mbedTLS などのセキュリティ・クリティカルな実務システムで、すでに大規模に採用されています。

F*（F Star）は「暗号・通信プロトコルの証明済み実装」という具体的な実務領域で、他に類を見ない深さと広がりを持っているのです。

その一方でLean 4 は、数学の形式化（Mathlib、AlphaProof）や、汎用プログラミングの分野で強い存在感を示しています。

Python では実現が難しい、F* の力が発揮される場面 ── 実務のユースケース

*「F で何ができるのか」**を、これまで Pythonプログラマの皆様の目線で具体的にお伝えします。

ユースケース１ ── 暗号ライブラリの実装

皆様が、AES-GCM（Galois/Counter Mode）という暗号アルゴリズムを Python で実装したとします。

動作するコードは書けるでしょう。

しかし、「このコードは、いかなる入力に対しても、暗号仕様通りに正しく動く」ことを、皆様は保証できるでしょうか。

Python でこの保証を得るには、大量のテスト・ケースと、経験豊富なレビューアの目に頼ることになります。

しかし、暗号ライブラリのバグは、時に致命的な脆弱性として、皆様の顧客の秘密情報を危険に晒します。

F*言語を採用することで、暗号アルゴリズムの正しいことの証明をコードの中に記述することができます。

例えば、AES-GCM の実装が、「メモリ安全である」「機能的に正しい」「タイミング側面攻撃に耐性がある」ことを、コードの型として記述し、F*（F Star）コンパイラによって、あらゆる入力に対して正しく動くかを検証させることができます。

この仕組みで作られたのがHACL*という検証済み暗号ライブラリです。

HACL* は、Curve25519、Ed25519、AES-GCM、ChaCha20、Poly1305、SHA-2、SHA-3、HMAC、HKDFなどの主要な暗号アルゴリズムの証明済み実装を提供しています。

そのコードは Mozilla Firefox、Linux カーネル、Tezos ブロックチェーンなどで、動いています**。

ユースケース２ ── バイナリ・パーサの生成

皆様が、TLS 1.3 のパケット・フォーマットのパーサを、Python で書いたとします。
動作するコードは書けるでしょう。

しかし、「悪意ある入力に対して、このパーサはバッファ・オーバーフローを起こさない」「不正な入力を、常に正しく検出する」ことを、皆様は保証できるでしょうか。

バイナリ・パーサの脆弱性は、しばしば深刻なセキュリティ問題を引き起こします。
Heartbleed も、Log4Shell も、パーサの脆弱性が根本原因の一つでした。

F*を採用すると、バイナリ・パーサを、証明済みの形で自動生成させることができるようになります。

EverParse というツールが、バイナリ・データ形式の仕様から、メモリ安全性と機能的正しさが証明済みのパーサを、C 言語で自動生成してくれるからです。

ユースケース３ ── TLS 1.3 の実装

皆様は、TLS 1.3 というWeb の通信を暗号化するプロトコルをご存じでしょうか？

TLS 1.3 の実装は極めて複雑で、しかも、そのバグは Web 全体のセキュリティを脅かすものです。

F*を採用すると、TLS 1.3 の完全な実装を、証明済みの状態で書きこむことができるようになります。

miTLS-fstar というプロジェクトが、TLS 1.3 の検証済み実装を F* で提供しています。

F* のコード例

F* のコードは、具体的にはどのようなものなのか、いくつか実例を見ていきましょう。

その前に、Python と F* の「保証のレベルの違い」を、一枚の図で整理しておきます。

Python の世界:
  コード ──> テストで保証 ──>「試した入力については、正しく動いた」
                              (テストしていない入力は、保証の対象外)

F* の世界:
  コード ──> 証明で保証   ──>「あらゆる入力に対して、正しく動く」
                              (数学的な証明として、コンパイル時に検証済み)

この違いを頭に置いた上で、コードを見ていきましょう。

まず、Python で「整数の絶対値を返す関数」を書いたコードを見て下さい。

def abs(x: int) -> int:
    if x >= 0:
        return x
    else:
        return -x

これを F* で書くと、次のようなコードになります。

val abs : x:int -> Tot int
let abs x = if x >= 0 then x else -x

ここまでは、まだ Pythonのコードとあまり変わりません。
F* の強みは、ここから先にあります。

F* では、返り値の性質を型に書き込むことができます。

val abs : x:int -> Tot (r:int{r >= 0})
let abs x = if x >= 0 then x else -x

このr:int{r >= 0}という記法が、篩型（ refinement type ） です。
「返り値rは、r >= 0を満たす整数である」という意味です。

この型を書くことで、F* のコンパイラは、実装が本当に「非負の整数を返す」ことを、自動的に検査してくれます。

万が一、実装が誤っていて、負の整数を返す可能性があれば、コンパイル・エラーで拒否してくれる ので、プログラマは誤りの存在に気付くことができます。

あらゆる入力に対して、この関数が非負の整数を返すことが、数学的に保証されるわけです。

Python でこの保証を得るには、大量のテスト・ケースを書き、それでもなお「テストしていない入力で失敗するかもしれない」という不安を残さなければなりません。

それがF*であれば、たった一行の型の記述で、あらゆる入力に対する保証が得られるのです。

一言で言えば

F* は、「証明指向プログラミング言語」という新しいカテゴリを代表する言語です。

関数型プログラミング、依存型プログラミング、形式検証、定理証明の技術を統合し、プログラムそのものが、その正しさの証明を内包することを可能にします。

F*（F Star）の限界 ── 他の定理証明・形式検証言語との役割分担

ここまで F*（F Star）の強みをご紹介してきましたが、公平を期すために、F*（F Star）の型システムでは実現が難しいこと、そして他の定理証明・形式検証言語の方が適している領域についても、正直にお伝えします。

万能の言語は存在しません。

F*（F Star）にも、明確な「得意でない領域」があります。

そして、その領域では他の言語たちが、それぞれの持ち場で力を発揮しています。

１. 数学そのものの形式化 ── Lean 4 の独壇場

現代数学の研究レベルの定理を形式化するという営みでは、Lean 4 が圧倒的な存在感を持っています。

その最大の理由は、Mathlib という巨大な数学ライブラリの存在です。

Mathlib には、代数・解析・位相・数論など、現代数学の広範な分野の定義と定理が、既に形式化されて蓄積されています。

新しい定理を形式化しようとするとき、その土台となる数学的概念が「すでに証明済みの部品」として揃っているかどうかは、決定的な差になります。

F*（F Star）には、Mathlib に相当する数学ライブラリはありません。

F*（F Star）のライブラリ資産は、暗号・パーサ・低レベルコードといったソフトウェア検証の方向に蓄積されており、純粋数学の方向には蓄積されていないのです。

「フェルマーの最終定理を形式化しよう」という話題で名前が挙がるのは Lean 4 であって、F*（F Star）ではありません。

これは優劣ではなく、蓄積の方向の違いです。

２. 証明の対話的な組み立てと、タクティクの成熟度 ── Rocq・Isabelle の年輪

Rocq（旧称 Coq）や Isabelle には、「タクティク（tactic）」と呼ばれる、証明を対話的に組み立てるための道具立てが、数十年分の厚みで蓄積されています。

証明の途中経過を一歩ずつ確認しながら、「この補題を適用する」「場合分けする」「帰納法を使う」といった指示を積み重ねて、複雑な証明を人間の手で丁寧に構築していく ── この対話的な証明開発の体験において、Rocq と Isabelle は長い歴史に磨かれた完成度を持っています。

Isabelle には、複数の自動証明器を束ねて補題を探し出す Sledgehammer という強力な自動化の仕組みもあります。

F*（F Star）にも Meta-F* というタクティクの仕組みは存在しますが、**F*（F Star）の証明スタイルの主軸は、あくまで「Z3 による自動判定」**です。

そして、ここに F*（F Star）の実務上の弱点が現れます。

Z3 が証明に失敗したとき、「なぜ失敗したのか」を突き止めるのが難しいのです。

SMT ソルバーは強力ですが、その判断過程は人間にとってブラック・ボックスに近く、証明が通らないときの試行錯誤（クエリの調整、補題の追加）には独特の経験が要求されます。

また、同じ証明が、ソルバーのバージョンや設定によって通ったり通らなかったりする「証明の不安定性」 も、F*（F Star）コミュニティ自身が認める課題です。

「証明の一歩一歩を人間が完全に制御し、理解しながら進めたい」場面では、Rocq や Isabelle に分があります。

３. 証明の検査基盤の小ささ ── 「何を信頼するか」の違い

定理証明の世界には、「証明の正しさを最終確認する部分（カーネル）は、できる限り小さくあるべきだ」 という思想があります（de Bruijn 基準と呼ばれます）。

検査する側が小さければ小さいほど、「検査する側そのものにバグがある」可能性を吟味し尽くせるからです。

Rocq、Lean 4、Agda、Isabelle は、この思想に沿って設計されており、小さなカーネルが証明の全体を検査します。

一方、F*（F Star）の証明の信頼は、型検査器に加えて、Z3 という大規模なソフトウェアへの信頼を含みます。

Z3 は世界中で使われ鍛え抜かれたソフトウェアですが、それでも「小さなカーネルだけを信頼すればよい」という体制と比べると、信頼しなければならない範囲（Trusted Computing Base）が大きいことは事実です。

数学基礎論に関わる証明や、「証明の証明可能性」自体が問われる場面では、この違いが重視されます。

４. 最先端の型理論の探究 ── Agda と Cubical Agda

ホモトピー型理論（HoTT）や Cubical 型理論といった、型理論の最先端の研究は、Agda（特に Cubical Agda）や Rocq を舞台に進められています。

F*（F Star）の型システムは、あくまで「実用のプログラムに証明を付ける」ことに最適化されており、型理論そのものの新しい地平を探究する道具としては設計されていません。

５. 大規模システム検証の金字塔 ── Isabelle と seL4

OS カーネル全体の機能的正しさを証明した seL4 マイクロカーネルは、Isabelle/HOL で検証されました。また、検証済み Cコンパイラの金字塔である CompCert は Rocq（Coq） で書かれています。

つまり、「セキュリティ・クリティカルなシステムの形式検証」という F*（F Star）の得意領域においてさえ、歴史的な大規模成果の多くは、Rocq や Isabelle の側にあります。

つまり、「大規模システムの形式検証」という歴史の中では、seL4 や CompCert という金字塔が先に打ち立てられており、F*（F Star）の Project Everest は、その後に登場した後発の挑戦者です。

後発ではありますが、Everest は「暗号・通信プロトコルの証明済み実装」という領域ですでに大規模な実績を挙げ、独自の地位を確立しています。

ただし、この分野の歴史的な代表作をすべて F*（F Star）が担っているわけではない
── その点は、公平に押さえておくべき事実です。

役割分担の全体像

以上を表に整理します。

言語	最も力を発揮する領域	代表的な成果・資産
*F（F Star）**	暗号・通信プロトコル・パーサの証明済み実装（証明指向プログラミング）	Project Everest、HACL*、EverParse、miTLS
Lean 4	数学の形式化、汎用プログラミング	Mathlib、AlphaProof
Rocq（旧 Coq）	プログラミング言語理論、検証済みコンパイラ、対話的証明	CompCert、Iris
Isabelle	古典的高階論理、大規模システム検証、強力な証明自動化	seL4、Sledgehammer、AFP
Agda	型理論の研究、ホモトピー型理論	Cubical Agda

使い分けの指針

読者の皆様が将来、これらの言語のどれかを選ぶ場面が来たときのために、指針を一言ずつでまとめます。

「動くシステムに、証明を付けて出荷したい」 ── F*（F Star）
「数学の定理を形式化したい」 ── Lean 4
「証明を一歩ずつ、完全に制御しながら組み立てたい」 ── Rocq、Isabelle
「型理論そのものを探究したい」 ── Agda

F*（F Star）は、「何でもできる言語」ではありません。

しかし、「数学的に証明済みのコードを、実際に動くシステムとして世に出す」
── この一点にかけては、他のどの言語にも代えがたい道具なのです。

限界を知ることは、その価値を正確に知ることでもあるのです。

依存型と篩型のハイブリッドという性格

本記事執筆者が公開済みのPythonの型ヒントの限界を超える「篩型」入門 ―― "x > 0" を型に書くと何が起きるのか（LiquidHaskell・F*・Typed Racket・Idris 2 への誘い）で、F* について**「依存型と篩型のハイブリッド」**と表現しました。

この表現が意味するところを、以下で詳しく解説します。

依存型と篩型は、何が違うのか

依存型と篩型は、いずれも「値の性質を型に書き込む」技術です。
しかし、その表現の仕方には、大きな違いがあります。

依存型(dependent types) は、型が、他の値に依存することを許します。

例えば、Vector Int nという型は、「長さが $n$ の整数のベクトル」を意味します。
ここでnは自然数の値であり、型Vector Int nは、このnという値に「依存」しています。

篩型（ refinement types ） は、型に、値が満たすべき論理的な条件（述語）を書き加えることで、値の性質を表現します。

例えば、x:int{x > 0}という型は、「x > 0を満たす整数x」を意味します。

両者の違いは、表現の柔軟性にあります。

依存型は、極めて柔軟な性質を表現できますが、その分、型検査は難しく、証明の負担が大きい傾向があります。

その一方で、篩型は、表現できる性質は限られますが、その分、証明の多くを自動化しやすい傾向があります。

F*は両者を統合した

F* の設計思想は、依存型と篩型の両方を、同じ型システムに統合するというものです。
皆様は、その場面に応じて、次のように使い分けることができます。

単純な性質（正の整数、範囲内の値など）は、篩型で表現し、SMTソルバーによる自動証明を活用する
複雑な性質（ソート済みのリスト、平衡二分木、暗号プロトコルの状態など）は、依存型で表現し、対話的な証明を活用する

この統合こそが、F の実務での使いやすさの、大きな源泉*です。
単純な保証は簡単に得られ、複雑な保証は必要に応じて厳密に証明できる、というバランスが取れています。

タロウくんと専任講師の対話 ── 依存型と篩型のハイブリッド

この節の主張が腑に落ちるように、以前公開しました形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界の登場人物、学部生のタロウくんと専任講師の対話を、抜粋の形でお届けします。

タロウくん
先生、F* が「依存型と篩型のハイブリッド」と紹介されているのを見ました。
この意味が、少し腑に落ちません。

専任講師
いい問いだ。

順に整理しよう。

依存型は、複雑な性質を柔軟に表現できるが、その分、証明を書く負担が大きい。

篩型は、単純な性質しか表現できないが、その分、SMT ソルバーが多くの証明を自動化してくれる。

F* は、この両方を統合した。
だから、皆様が場面に応じて使い分けられる。

タロウくん
なるほど。
両方が同居しているから、書き手が最適な道具を選べるのですね。

専任講師
そうだ。
これが、F* の実務での使いやすさの中核にある。

タロウくん
先生、両者は F*(F Star) のコードで書くと、それぞれどんな見た目になるんですか?

専任講師
抽象的な議論だけだとイメージはつかみづらかったね。
よし。コードを見ながら議論しよう。

まず、篩型で「正の整数のリスト」を表現すると、こうなる。

type pos_int = x:int{x > 0}
val positive_list : list pos_int
let positive_list = [1; 2; 3; 5; 7]

x:int{x > 0}という一行が、篩型の記法だ。

「x は整数で、かつ x > 0 を満たす」という条件を 型の中に 書き込んでいる。

この型を持つリストに、負の数を入れようとすれば、F*（F Star）コンパイラが型エラーで拒否してくれる。

証明の負担を、このコードを書いた人間は追わなくて済む。
SMT ソルバー(Z3)が自動で判定してくれるからだ。

タロウくん
なるほど、{x > 0}という条件の付け方が、篩型なんですね。

専任講師
そうだ。
次に、依存型 で「長さが n のリスト(ベクトル)」を表現すると、こうなる。

val vec : n:nat -> Type
let rec vec n =
  if n = 0 then unit
  else int & vec (n - 1)

val make_vec3 : vec 3
let make_vec3 = (1, (2, (3, ())))

vec nという型は、値n(自然数)に依存する型 だ。

vec 3と書けば「長さがちょうど 3 のベクトル」を意味する型となり、
vec 5と書けば「長さがちょうど 5 のベクトル」を意味する型となる。

値nによって、型そのものが変わる ── これが「型が値に依存する」ということだ。

タロウくん
篩型の方が、たしかに書きやすそうに見えます。

専任講師
君もそう思うかい？
君の感覚は、篩型と依存型を併用している技術者によって共有されているのと同じ感覚だ。

単純な性質（正の整数、範囲内の値、長さの下限など）は、篩型で書けば、SMT ソルバーが自動で確かめてくれる。

その一方で、リストの長さそのものを型に反映させたい場面や、証明の中身が複雑になる場面では、依存型の柔軟性が必要となる。

F*（F Star）では、この両方を、同じコードの中で混ぜて使えるんだ。

タロウくん
それが「両者の統合」の意味なんですね。
腑に落ちました。

タロウくん
先生、ということは、F*（F Star）のプログラマも、簡単な記法で表現できる篩型で実現できる部分は F*（F Star）の篩型の記法を選択し、依存型でないと実現できないケースでは、F*（F Star）の依存型の記法を選択する、という使い分けをしているのですか？

どちらを選択するにせよ、F*（F Star）という同じ言語の中で選択できるのが強み なのですね？

専任講師
そのとおりだ。

F*（F Star）プログラマは、君がイメージしてくれたように、まず最初に篩型で書けないかどうかを試す。

SMTソルバーが自動で証明を通してくれる限りは、篩型の方が書き手の負担が圧倒的に軽いからだ。

篩型では表現しきれない性質 ── たとえばリストの長さそのものを型に反映させたい、あるいは複数の値の関係を型のレベルで表したい ── に直面したとき、そこで初めて依存型に手を伸ばす。

タロウくん
段階的に、必要な分だけ強い道具に切り替えていく のですね。

専任講師
そうだ。

そして、篩型と依存型を別の言語に分かれて実装するのではなく、F*（F Star）という一つの言語の中で、同じ構文の系譜で選べる。

ここに F*（F Star）の設計思想の強みがある。

書き手は、道具を切り替えるために言語を移動する必要がない。

同じファイルの中で、簡単な性質は篩型で軽く済ませ、複雑な性質だけ依存型で厳密に書く、という混在が自然にできる。

F*（F Star）はどんな経緯で生まれたのか

INRIA と Rocq（旧称 Coq）── 定理証明系の歴史

F* の物語は、**INRIA(Institut National de Recherche en Informatique et en Automatique、フランス国立情報学自動制御研究所)**という、フランスの国立研究機関から始まります。

INRIA は、コンピュータ・サイエンスと応用数学の分野で、世界的に極めて重要な研究機関です。

プログラミング言語の分野では、OCaml（現在の関数型プログラミング言語の主要な一つ）の生みの親 であり、そして、Rocq（旧称 Coq）という、世界で最も影響力のある定理証明系の一つの生みの親 でもあります。

Rocq（旧称 Coq）は1984年に、INRIA の Gérard Huet と Thierry Coquand によって開発が始まりました。

当時は、CoC（ Calculus of Constructions ）」と呼ばれ、後に「Coq」という名前になります。

Coq という名前は、開発者の一人 Coquand の名前と、フランス語の「雄鶏（coq）」に由来する遊び心のあるネーミングでした。

ロゴにも雄鶏が使われています。

Coq は 1991 年に「Coq」という名前で正式に登場し、2013 年には ACM SIGPLAN プログラミング言語ソフトウェア賞を受賞する成熟した定理証明系となりました。

そして、2023 年に、より国際的なアイデンティティのため、Rocq への改名が発表されるに至ります。

INRIA は、定理証明系の分野で世界を主導する研究機関の一つなのです。

Microsoft Research と INRIA の共同研究センター

Microsoft Research は、Microsoft社の研究部門です。

プログラミング言語の研究、特に関数型プログラミング言語 F# や、依存型言語 Dafny、そして 定理証明系 Lean（現在は主に Amazon 傘下の Leanprover Community が開発を主導）の開発 に関わってきました。

Microsoft ResearchとINRIA は、 2005年に共同研究センター（ Microsoft Research-INRIA Joint Centre ）の設立に合意し、2006年頃から実質的な活動を開始しました。

この共同研究センターは、パリ近郊のオルセー（Orsay） に置かれ、形式手法、コンピュータビジョン、機械学習、プライバシー、暗号、分散システムなどを研究テーマ としています。

研究員は、INRIA 側 40名、Microsoft Research 側 30名、非常勤 30名の合計 100名という規模です。

F* は、この Microsoft Research-INRIA Joint Centre の共同プロジェクトの一つとして、2011年に登場します。

なぜ Microsoft は F* をはじめとする定理証明・形式検証系の言語開発に取り組むのか

「営利企業である Microsoft が、なぜ直接の売上を生まない研究言語の開発に、長年にわたり多額の投資を続けているのか」 という疑問を、皆様は当然お持ちになると思います。

理由は、Microsoft の主力事業のリスク構造と密接に結び付いているからだと考えられます。

Microsoft の主力事業は、Windows・Office・Azure クラウド・Xbox・GitHub・LinkedIn を含む膨大な数のソフトウェア・システムです。

これらのシステムのバグや脆弱性は、顧客のデータ漏洩、集団訴訟、当局からの制裁金、ブランドの毀損、株価の下落という形で、直接に Microsoft の業績を直撃します。

１件の重大な脆弱性が発覚するだけで、数百億円規模の損失を招くことも珍しくありません。

F*(F Star)、Dafny、Lean などの言語で開発された「証明済みコード」を Microsoft の主力製品の内部に組み込むことで、Microsoft は将来の脆弱性発覚のリスクを、事前に大幅に減らすことができます。

バイナリ・パーサの自動生成ツール EverParse は、Microsoft Azure の仮想化基盤 Hyper-V の内部で、Azure クラウドを通過するすべてのネットワーク・パケットの解析と検証に既に採用されています。

Azure の顧客(米国国防総省、欧州の各国政府、世界の主要金融機関を含む)にとって、「Microsoft のクラウド基盤は数学的に正しさが証明されたコードで動いている」という事実は、他社クラウドとの決定的な差別化要因となります。

もう一つの経営的な狙いは、世界最高峰の研究者の確保です。

Microsoft Research は 1991 年に Bill Gates と Nathan Myhrvold が IBM Research や Bell Labs をモデルに設立した基礎研究部門で、直接の製品化を目的とせず長期投資として運営されています。

Nikhil Swamy 氏、Cédric Fournet 氏、Karthikeyan Bhargavan 氏、Leonardo de Moura 氏をはじめとする世界最高峰の研究者を、F*（F Star）やLeanなどの魅力的な研究プロジェクトを通じて Microsoft Research に集めることで、Microsoftは、世界の技術潮流の最前線に居続けること ができています。

「短期の販売による直接利益」ではなく、「長期の主力事業のリスク削減」「クラウド事業の競争力強化」「世界最高峰の人材の獲得」 という３つのリターンが、Microsoft が F*(F Star) の開発に長年投資を続けている経営上の理由です。

【コラム】なぜ日本・韓国・中国・ロシアの企業からは、世界的に普及する言語が生まれてこないのか(クリックで展開)

Microsoft や Google のような米国企業が、C・C++・Go・Java・Python・JavaScript・Rust・Swift をはじめとする世界の主要プログラミング言語を送り出してきた一方、日本・韓国・中国・ロシアの企業から世界的に普及した言語は、極めて限られています。

日本発の言語で、世界的に普及した希少な事例としては、次の2つが挙げられます。

Ruby ── まつもとゆきひろ氏が1993年から個人で開発、1995年に公開。2004年に David Heinemeier Hansson 氏が Web フレームワーク Ruby on Rails を発表したことで、世界的に爆発的に普及しました。
TRON(トロン) ── 坂村健氏(当時東京大学)が1984年に発表した組込みシステム向けのオペレーティング・システム仕様。自動車のエンジン制御、家電製品、産業機器の内部で、世界的に広く採用されています。

しかし、Ruby と TRON を除けば、日本発の世界的な言語の事例は極めて乏しく、韓国・中国・ロシア発の言語に至っては、世界的な広がりを持つ事例がほぼ見当たらないというのが実相です。

日本には NTT、NEC、富士通、日立、東芝、三菱電機など、世界水準の研究所を国内外に複数擁する巨大企業が数多く存在します。

NTT 電気通信研究所(1948 年源流)、NEC 中央研究所(1939 年設立)、富士通研究所(1968 年設立)は、いずれも Microsoft Research の設立年(1991 年)よりも遥かに古く、半世紀から 80 年以上にわたり基礎研究への長期投資を続けてきました。

スーパーコンピュータ「京」「富岳」(理化学研究所と富士通の共同開発)、光通信技術、半導体、暗号理論、量子コンピュータの基礎研究など、世界水準の技術成果を継続的に送り出しています。

それにもかかわらず、これらの日本企業からは、Ruby と TRON を除いて、世界に広がる汎用プログラミング言語がほとんど生まれてこないという現象があります。

その構造的な理由として、筆者は次の5点を考えています。

理由１ ── 研究成果の対象領域の違い

日本企業の研究所は、暗号理論、計算量理論、光通信、量子暗号、半導体、スーパーコンピュータのハードウェア設計、モバイル通信規格といった、特定の応用領域の高度化に長期投資を続けてきました。「京」「富岳」のスーパーコンピュータは、そのハードウェア設計の到達点として、世界最高峰に長年位置しています。

その一方で、プログラミング言語という汎用の基盤技術は、日本企業の研究所の予算配分の中で、伝統的に主要な位置に置かれてこなかったという事実があります。

企業の中で、どの領域に長期の研究予算を配分するかという経営判断がこの結果に大きく作用しています。

理由２ ── 研究成果の商用化における戦略の違い

日本企業は、基礎研究の成果を**「自社のハードウェアや通信インフラの競争力強化に還元する」**という戦略が主流でした。

**「研究成果を自社の製品の中に組み込み、その製品を売ることで研究投資を回収する」**というモデルです。

一方、米国企業(特に Google、Microsoft、Facebook、Mozilla)は、**「基礎研究の成果を、オープンソース言語として世界に無償公開し、世界の開発者コミュニティを自社のプラットフォームの生態系に取り込む」**というプラットフォーム戦略を採りました。

Go 言語(Google)、Rust(Mozilla)、TypeScript(Microsoft)、React(Meta)などは、**「無償公開して世界のエコシステムを主導し、そこから間接的に自社のクラウドや広告や開発者採用に還元する」**という間接的な収益モデルの上に成り立っています。

この間接的なプラットフォーム戦略は、日本企業では相対的に採られてこなかったというのが実情です。

理由３ ── 英語のコミュニティ形成の壁

プログラミング言語のドキュメント、規格、コミュニティは、事実上すべて英語で構築されます。

Ruby ですら、1995年の公開から2000年に英語の書籍「Programming Ruby」が出るまで、5年もの間、日本国内での普及にとどまっていました。

母語が英語ではない国の技術者が世界的なコミュニティを最初から築くには、この言語障壁が構造的な足かせとなります。

理由４ ── 産学連携で世界コミュニティを主導する経路の細さ

米国では、Bell Labs の C、Xerox PARC の Smalltalk、Sun Microsystems の Java、Google の Go、Microsoft Research の F#・F*・Dafny・Lean、Mozilla の Rust といった具合に、企業の基礎研究部門が、社外の学術研究コミュニティと有機的に接続し、その成果を世界のオープンソース・コミュニティへと橋渡ししてきました。

日本の巨大企業の研究所は、社内向けの技術開発と、政府・国家プロジェクトへの参加が中心となる傾向があり、社外の世界的なオープンソース・コミュニティを主導する経路が、米国企業と比較して構造的に細いという特徴があります。

理由５ ── オープンソース文化の歴史の浅さ

米国では 1980 年代の FSF・GNU プロジェクト、1990 年代の Linux、その後の GitHub と、言語開発を世界規模で協業するオープンソース文化のインフラが 40 年以上にわたって蓄積されてきました。

日本・韓国・中国・ロシアでは、この歴史的な蓄積が相対的に浅く、世界規模のオープンソース・プロジェクトを主導する経験値も限られています。

日本の巨大企業は、Microsoft Research を遥かに超える歴史を持つ基礎研究所を擁し、ハードウェアと通信インフラの分野で世界水準の研究成果を送り出しながらも、プログラミング言語という汎用基盤技術への予算配分の少なさ、そして「無償公開して世界コミュニティを主導するプラットフォーム戦略」を採ってこなかったという戦略選択により、Ruby と TRON を除けば、世界的な言語を送り出すには至っていない、というのが筆者の見立てです。

F* の生まれた経緯 ── 2011年、ICFP 論文

F* の最初の姿は、2011年に開催された ICFP（ International Conference on Functional Programming ）で発表された論文 "Secure Distributed Programming with Value-Dependent Types として世に出ました。

著者は Nikhil Swamy、Juan Chen、Cédric Fournet、Pierre-Yves Strub、Karthikeyan Bhargavan、Jean Yang の６名です。

この論文が、F* の初代設計の基準論文となります。

その後、2016年にPOPL（ Principles of Programming Languages ）で発表された論文 "Dependent Types and Multi-Monadic Effects in F*" が、現代の F* の設計を確立した基準論文 となります。

ここで、F* は依存型とモナディック・エフェクトを統合した証明指向プログラミング言語としての姿を獲得したのです。

開発の動機は何だったのか

F* の開発の主要な動機は、次のように整理できます。

「対話的定理証明系（Rocq、Lean など）は、極めて強い保証を提供できるが、実用のシステム・プログラミングには使いにくい。

他方で、汎用の関数型プログラミング言語（OCaml、Haskellなど）は、実用のシステム・プログラミングに使えるが、証明の強さでは対話的定理証明系に及ばない。

この２つのギャップを埋める言語を作ろう」

この動機 は、特にセキュリティ・クリティカルなソフトウェア開発の分野で、切実なものでした。

TLSプロトコルの実装、暗号ライブラリ、分散システムの安全性。

これらは、「厳密に証明された正しさ」と「実用で動く性能」の両方が必要な領域 です。

しかし、当時、この２つを同時に満たす道具は事実上、存在しませんでした。

F* は、このギャップを埋めるための、Microsoft Research と INRIA の共同挑戦だった のです。

なぜ INRIA と Microsoft が組んだのか

INRIAは、Rocqを生んだ世界的な定理証明系の研究拠点であり、その分野の学術的な蓄積は極めて厚い ものでした。

その一方で、Microsoft Researchは、実用のシステム・プログラミングと業界における展開力 を持っていました。

両者が組むことで、学術的な深さと産業的な広がりを兼ね備えたプロジェクトが可能になると判断されたのです。

F は、まさに「学術と産業の橋渡し」を体現するプロジェクト*でした。

目的は果たされたのか

目的は、少なくとも部分的には果たされたように思います。

Project Everest という、F* を用いた「検証済み HTTPS スタック」の構築プロジェクトがMicrosoft Research 中心で進行し、その成果が次のような形で実用に展開されているからです（次節で詳しく扱います）。

Mozilla Firefox にF* で証明された暗号ライブラリ HACL* のコードが組み込まれた
Linux カーネル にF* で証明された EverCrypt のコードが組み込まれた
Tezos ブロックチェーン、ElectionGuard 電子投票 SDK、WireGuard VPN、mbedTLS など多くの実用システムにF*で証明されたコードが動いている

「対話的定理証明系のような強い保証を、実用のシステムで動くコードとして提供する」という F* の目的は、これらの実例において達成されているとみなすべきです。

現在も進化を続けている

F* は、2011年の初登場以来、継続的に進化しています。

2026年4月18日には、最新版 v2026.04.17 がリリースされ、活発な開発 が続いています。

ライセンスは Apache 2.0で、商用利用にも制限がありません。

Pulse という並行分離論理（ concurrent separation logic ）を F* に組み込んだDSL も 2021-2023 年頃に導入 され、POPL 2024 で発表されました。

並行プログラムの検証という難しい分野に、F* は挑（いど）み続けているのです。

F*（F Star）の用途と実際の利用実績

Project Everest ── F* の主要な用途

F* の主要な用途は、Project Everest という、Microsoft Research 中心の大規模プロジェクトです。

このプロジェクトは、「Web の通信を暗号化する仕組み HTTPS(皆様が Web ブラウザで https:// から始まる Web サイトを見るとき、通信内容を暗号化して盗聴や改ざんから守る技術) の実装全体を、F*(F Star) で数学的に正しさを証明した上で構築する」ことを目標とする極めて野心的なプロジェクトです。

Project Everest の構成要素を順に紹介します。

F* : 核心となる証明指向プログラミング言語
HACL* : 検証済み暗号プリミティブのライブラリ(Curve25519、Ed25519、AES-GCM、ChaCha20、Poly1305、SHA-2、SHA-3、HMAC、HKDF など)
EverCrypt :HACL* と ValeCrypt を統合した検証済み暗号プロバイダ(実行環境に応じて自動的に最速の実装を選択)
Vale(ValeCrypt) : 高性能な検証済みアセンブリ・コード生成ツール
Low と KaRaMeL* :F* の低レベル・サブセット(Low*)と、Low* から読みやすい C コードへ変換するツール(KaRaMeL、旧称 KReMLin)
EverParse : バイナリ・データ形式のパーサとシリアライザを証明済みの形で自動生成するツール
miTLS-fstar : F* での TLS 1.3 の検証済み実装
EverQuic-crypto : QUIC プロトコルの検証済み暗号実装

これらすべてが、F* を核とする一つの生態系を形成しています。

HACL* のコード実例 ── Firefox で動く暗号関数の型

Project Everest の中核である HACL* のコードが実際にどう見えるか、皆様の目でお確かめください。Firefox の中で日々動いている、Curve25519(楕円曲線暗号の一つ)のスカラー倍算関数の型のシグネチャです。

val scalarmult:
    out:lbuffer uint8 32ul       // 結果を書き込む 32 バイトのバッファ
  -> priv:lbuffer uint8 32ul     // 秘密鍵(32 バイト)
  -> pub:lbuffer uint8 32ul      // 公開鍵(32 バイト)
  -> Stack unit
    (requires fun h ->
      live h out /\ live h priv /\ live h pub /\
      disjoint out priv /\ disjoint out pub)
    (ensures fun h0 _ h1 ->
      modifies (loc out) h0 h1 /\
      as_seq h1 out ==
      Spec.Curve25519.scalarmult (as_seq h0 priv) (as_seq h0 pub))

requires の部分が、関数の呼び出し時に成り立っていなければならない条件(メモリ上に3つのバッファが確保されており、互いに重ならないこと)です。

ensures の部分が、関数の実行後に成り立つ保証(out バッファに、秘密鍵と公開鍵から数学的な仕様通りに計算されたスカラー倍算の結果が書き込まれていること)です。

この型のシグネチャは、Curve25519 の数学的な仕様(Spec.Curve25519.scalarmult)と、実装コードの動作が完全に一致することを、F*(F Star) コンパイラが機械的に検査してくれます。

皆様が Firefox で https:// から始まる Web サイトを見るたびに、この証明済みコードが皆様の通信を守っているわけです。

2026年7月末時点までの世界各国での利用実績

Project Everest の成果は産業界や私たちの日常生活を支える複数の社会公共システムの中で日夜稼働し続けています。

１. Mozilla Firefox

Mozilla Firefox は、世界で広く使われている無料の Web ブラウザです。その暗号ライブラリ NSS(Network Security Services)には、HACL のコードが組み込まれています*。皆様が Firefox を使うたびに、F* で証明された暗号コードが、皆様の通信を守っています。

２. Linux カーネル

Linux カーネルは、サーバー、Android スマートフォン、組み込み機器などで、世界的に広く使われているオープンソース OS の中核です。その内部に、EverCrypt のコードが組み込まれています。皆様がお使いの Linux サーバーや、Android デバイスの中で、F* で証明された暗号コードが動いています。

３. Tezos ブロックチェーン

Tezos は、スマート・コントラクト(自動実行される契約プログラム)を扱えるブロックチェーン・プラットフォームの一つです。そこには、HACL のコードが暗号プリミティブとして使われています*。ブロックチェーンの正しさは、暗号の正しさに依存します。F で証明された暗号は、この基盤を強固にしています*。

４. ElectionGuard 電子投票 SDK

Microsoft の ElectionGuard は、電子投票の完全性（投票が正しく集計されたかの検証）を可能にするための、オープンソースの開発キット(SDK) です。

ここでも、F* で証明された暗号コードが使われています。

民主主義の根幹である選挙の完全性を、形式的に検証された暗号で守ろうとする試みです。

５. WireGuard VPN

WireGuard は、Linux カーネルに標準採用された高速で安全な VPN(仮想プライベート・ネットワーク、遠隔から社内ネットワークに安全に接続する仕組み)プロトコルです。

ここでも、F* で証明された暗号コードが使われています。

６. mbedTLS

mbedTLS は、組み込みシステム（IoT 機器、家電、自動車の車載システムなど)でよく使われる、軽量な TLS（Web 通信の暗号化）ライブラリの一つです。

F* で証明されたコードが稼働しています。

INRIA/Microsoft が意図した用途との比較

INRIAとMicrosoftがF* に期待した用途は、「対話的定理証明系のような強い保証を、実用のシステムで動くコードとして提供する」ことでした。

上記の実績を見ると、この目的は、特に暗号ライブラリと通信プロトコルの分野で、極めて明確な形で達成されていると評価できます。

F* は、「机上の学術的な言語」ではなく、「実務のセキュリティ・クリティカルなコードの中で動く言語」という立ち位置をすでに確保しています。

その一方で、F* は、汎用プログラミング言語としては、Python や Rust や Go のように広く使われているわけではありません。

F* の強みは、証明の負担を受け入れる価値がある領域 ── つまり、正しさが極めて重要な領域 ── に集中しています。

しかしこの状況は、F* の設計思想 ── 「証明指向プログラミング」── からもたらされる当然の帰結なのかもしれません。

全体を俯瞰する

Project Everest とそこから広がる F* の生態系は、「証明指向プログラミングが社会公共システムを支える基盤技術足りうる」ことを実例として示していると言えます。

そして、この実例こそが、F* を学ぶ実務的な意味の、最も強固な根拠なのです。

我が国で F*（F Star）の認知度が低い理由と世界各国における存在感

日本での F*（F Star）の認知度が低い理由：筆者の見解

和文（日本語）で F*（F Star）の情報が極めて少ない理由について、筆者は次のように考えます。

【理由１】 F*（F Star）の主要な用途が「Web ブラウザ、OS、通信プロトコル、暗号ライブラリ」などの基盤レベルのインフラ層に集中していること

F*（F Star）の主要な用途は Project Everest です。

Project Everest の成果は、Firefox、Linux、WireGuard、Tezos、ElectionGuard、mbedTLS などのインフラ層で動いています。

**これらは「Web アプリケーション開発者から遠い、低レイヤーのインフラ層」**です。

我が国（日本）の IT エンジニアの主流は、Web サービス、業務システム、モバイルアプリの開発であり、インフラ層の暗号や通信プロトコルの実装に、直接関わる機会は少ないのが実情です。

このことが、F*(F Star) を実務で使う場面が、日本のエンジニアの多くにとって、身近に感じられない可能性として考えられます。

【理由２】日本の大学における形式手法の研究の相対的な位置

日本の大学でも、東北大学、京都大学、筑波大学、東京大学、産業技術総合研究所などで、形式手法・定理証明の研究が続けられています。

しかし、F*（F Star）を主題とする研究は、Coq、Isabelle、Lean などと比較して、日本の大学ではまだ盛んではありません。

Coq(現 Rocq)は日本の大学で長く研究されてきた経緯があり、日本語の書籍も存在しますが、F*（F Star）の日本語書籍はまだ出版されていません。

【理由３】 Microsoft Research と INRIA の共同開発言語という特異な出自

F*（F Star）は、Microsoft と欧州(フランス)の共同開発という、日本の IT エンジニアの主流の関心から離れた出自を持ちます。

日本のIT エンジニアの多くは、シリコンバレー系（Google、Meta、Amazon）や、日本国内のオープンソース・コミュニティ（Ruby、Rust、TypeScript）に強い関心を持つ傾向があります。

F*（F Star）は、この主流の関心の系譜からやや離れた位置にあり、認知度が低いのは、この文脈からも説明することができます。

世界的に認知度が低いF*（F Star）を学ぶ価値はあるのか

本記事執筆者は「学ぶ価値がある」と考えます。

以下にそう考える理由を述べます。

【理由１】 AI Agent 時代における形式検証の価値の高まり

AI Agent が生成したコードの正しさをどう保証するかは、今後の実務で決定的に重要な問いです。

F*（F Star）の GitHub 公式リポジトリは、Claude Code や GitHub Copilot CLI での F*（F Star）使用を推奨しています。

AI Agent × 形式検証という新しい潮流の最前線に、F*（F Star）はすでに立っているのです。

【理由２】「認知度が低い技術」だからこそ、早めに知っておくと人材価値が高まる

日本語圏における F*（F Star）の情報が少ないということは、逆に言えば、日本で F*（F Star）を実務で扱える人材は極めて希少だということです。

今後、我が国の産業界でも、暗号・通信プロトコル・ブロックチェーン・電子投票・電子政府などの分野で、「厳密に証明されたコードへの需要」 が高まる可能性は決して低くありません。

認知度が低い今こそ、F*（F Star）を学ぶことは、実務者としての希少な位置を占める好機と言えます。

欧米での F*(F Star) の存在感

欧米ではMicrosoft Research と INRIA を中心に、F*(F Star) は形式検証の実務を担う言語として大きな存在感 を誇っています。

Microsoft Research(米国 Redmond、英国 Cambridge) ── F*(F Star) の主要な開発拠点。Project Everest を主導。
INRIA(フランス、パリ近郊オルセー) ── F*(F Star) の共同開発拠点。Microsoft Research-INRIA Joint Centre として、100名規模の研究者が共同研究を行っています。
Mozilla(米国、Firefox) ── HACL* を採用。Firefox のユーザー全員が、F(F Star) の恩恵を受けています*。
Cornell University、Carnegie Mellon University、MIT ── 米国の主要大学でも、F*(F Star) を用いた研究が行われています。
オランダ、ドイツ、スイスの大学・研究機関 ── 欧州でも、F*(F Star) を用いた形式検証の研究が広がっています。

このように、欧米においては、一定の人数を擁する質の高いF*(F Star)コミュニティがすでに築かれています。

それではなぜ、欧米圏でも F*（F Star）を扱う個人ブログや企業技術ブログは少ないのでしょうか？

筆者が考える理由は次の３点です。

【理由１】

F*（F Star）を扱える技術者は暗号ライブラリ・通信プロトコル・OS カーネルといった深層のインフラを実装する現場に集中しています。

これらの職域に従事する技術者は、仕事で日常的に使用する言語について、個人ブログ記事を発信する個人的な動機を持たない可能性が考えられます。

彼らの職場は、社会インフラを基底レベルで支える縁の下の力持ちであるため、個人ブログ記事を書いたとしても他の職種で働いている大多数のブログ記事の読み手が関心を示さないと考えている節があるためです。

【理由２】

F*（F Star）は Microsoft Research と INRIA の研究プロジェクトの一環として開発が続けられている言語です。

言語仕様や機能追加の決定は、Nikhil Swamy 氏(Microsoft Research)と Cédric Fournet 氏、Chantal Keller 氏、Karthikeyan Bhargavan 氏、Aseem Rastogi 氏、Guido Martínez 氏らの研究者を中心とした極めて限定的なコミュニティによって進められています。

言語仕様の議論も、GitHub の Issue と Zulip のチャット・プラットフォームに集中しており、外部の一般エンジニアがコミュニティに関わる敷居が高いという構造があります。

こうした事情が、PythonやJavaのように、世界中の技術者がそれぞれ独自の使い方を編み出し、その経験談を個人ブログとして発信するというエコシステムが、F*（F Star）については未だに形成されていない背景にあるように思われます。

中国での F*（F Star）の存在感

中国では、清華大学、北京大学、上海交通大学、中国科学院などの主要研究機関で、形式検証・定理証明の研究が急速に進んでいます。

F*（F Star）単体を主題とする研究は、Coq や Lean と比較すると、まだ主流ではありません。

しかし、中国政府がスローガンとして掲げる「Prove, Don't Demo」（証明せよ、実演するな） は、F*（F Star）を含む形式検証全般の重要性を国家戦略として位置付ける方向性を示しています。

中国国内でも、F*(F Star) の学習リソースの整備が徐々に進んでいます。

中国語圏で確認できる主な学習リソースは、次のとおりです。

CSDN（中国最大級のプログラマ・コミュニティ）の F* 解説記事「探秘 FStar:一个高级形式验证的 ML 方言」(2024年3月)
CSDN の KaRaMeL 解説記事「KaRaMeL:从F*到C的低级程序提取工具」（2024年9月、F* から C 言語への抽出ツール KaRaMeL の中国語解説）
GitCode 博客の F* 教程「F* 编程语言教程」（2024年9月、冯爽妲Honey氏、インストール手順と Hello world のコード付き）
OSCHINA（中国オープンソース技術コミュニティ）の F* ページ（F* 公式書籍「Proof-Oriented Programming In F*」の中国語での紹介）
万维易源（showapi.com）の F* 解説記事「深入探索 F* 编程语言」（2024年10月、単子効応・依存型・精細化型の中国語での解説）
Gitee（中国の GitHub 互換のコード・ホスティング）の F* リポジトリのミラー版（F* GitHub 公式リポジトリを毎日同期し、中国国内からのダウンロード速度を高速化）

中国の技術者による F* の個人ブログ記事の総数は、筆者が web で確認できた範囲では、CSDN・GitCode 博客・万维易源・OSCHINA を合計しても 5〜6本程度にとどまります。

中国国内では、PythonやRustの中国語ブログ記事が数千から数万本規模で存在する中、F* の中国語ブログ記事は 5〜6本程度という圧倒的な少なさです。

結論として、中国の技術者による F* の個人ブログ記事の本数も、欧米や日本の状況と大きくは変わらず、極めて少ない水準にとどまっています。

なお、中国企業の技術ブログ記事で F* を主題としたものは、筆者がwebで確認できた範囲では見つかりませんでした。

ロシアでの F*(F Star) の存在感

ロシアには、伝統的に強い数理論理学・形式検証の学術的な蓄積があります。

モスクワ大学、サンクトペテルブルク大学、Steklov 数学研究所などで、定理証明・型理論の研究が続けられており、F*（F Star）を含む依存型言語への理解の深さは、世界屈指の水準にあります。

ロシアには Habr(ハブル) というロシア最大級の技術ブログ・プラットフォームがあります。

Habr で F*（F Star）を主題または副題として扱ったロシア語記事は、筆者が web で確認できた範囲では 2〜3本程度にとどまります。

"F* – новый язык с зависимыми типами для .Net"（F* – .Net 向けの依存型言語）（Habr、5,400 閲覧）
"Зависимые типы — будущее языков программирования"（依存型はプログラミング言語の未来）（Habr、Idris・JavaScript と並べて F* にも言及）

Habr 上には Python の記事が数万本、Rust の記事が数千本蓄積されている中で、F*（F Star）の記事は 2〜3本という圧倒的な少なさです。

ロシア企業の技術ブログ記事で F*（F Star）を主題としたものは、筆者が web で確認できた範囲では見つかりませんでした。

結論として、ロシアの技術者による F（F Star）の個人ブログ記事の本数も、欧米・日本・中国と同様に極めて少ない水準にとどまっている*という状況です。

韓国での F*（F Star）の存在感

韓国では、KAIST、POSTECH、ソウル大学などで、プログラミング言語・型理論の研究が盛んです。

特に、サムスン電子、LG 電子、SK ハイニックスなどの大手企業が、システムの正しさの検証のために形式手法への投資を強めており、F*（F Star）を含む形式検証言語への関心が高まっています。

韓国では velog.io、tistory.com、Naver ブログといった主要な技術ブログ・プラットフォームがあります。

しかし、これらのプラットフォームで F*（F Star）を主題または副題として扱った韓国語記事は、筆者が web で確認したかぎり見つかりませんでした。

韓国国内でも、Python の記事が数万本、Rust の記事が数千本蓄積されている中で、F*（F Star）の記事は事実上ゼロに近いという状況にあります。

韓国企業の技術ブログ記事で F*（F Star）を主題としたものも、筆者が web で確認した範囲では見つかりませんでした。

結論として、韓国の技術者による F*（F Star）の個人ブログ記事の本数は、欧米・日本・中国・ロシアと比較しても、極めて限定的な水準にとどまっているという状況です。

インドでの F*（F Star）の存在感

インドは、IIT(インド工科大学)、IISc(インド科学大学院)などで、プログラミング言語・形式手法の研究が世界水準にあります。

特に、Microsoft Research India(バンガロール)は、F(F Star) を含む形式検証の研究の重要な拠点*の一つです。

インドの IT エンジニアの層の厚さから、F*(F Star) の実務者コミュニティは、今後、急速に拡大する可能性があります。

インドは、 Microsoft Research India（バンガロール）に F*（F Star）の主要開発者の一人である Aseem Rastogi氏が所属するなど、学術研究の面では F*（F Star）の重要な拠点の一つとなっています。

しかし、インドの技術者による F*（F Star）の個人ブログ記事は、筆者が web で確認できた範囲では明確には見つかりませんでした。

インド国内では Medium・dev.to・Hashnode といった主要な技術ブログ・プラットフォームで、Python の記事が数万本、Rust の記事が数千本蓄積されている中で、F(F Star) の記事は事実上ゼロに近い*という状況です。

インド企業（Infosys、TCS、Wipro、Tech Mahindra などの大手 IT サービス企業）の技術ブログ記事で F*F Star）を主題としたものも、筆者が web で確認できた範囲では見つかりません。

イスラエルでの F*（F Star）の存在感

イスラエルは、サイバーセキュリティと暗号の研究で世界を主導する国の一つです。

Weizmann Institute of Science、Technion(イスラエル工科大学)、テルアビブ大学などで、形式検証・暗号プロトコルの研究が盛んに行われています。

イスラエルのスタートアップ（サイバーセキュリティ企業、暗号技術企業） では、F*（F Star）を含む形式検証言語への関心が、実務の水準で高いと考えられます。

イスラエルは Weizmann Institute of Science、Technion、テルアビブ大学などで、暗号研究と形式検証の世界的な拠点 として知られています。

しかし、イスラエルの技術者によるヘブライ語または英語での F*(F Star) の個人ブログ記事は、筆者が web で確認できた範囲では明確には見つかりませんでした。

イスラエル国内では英語圏の技術ブログ・プラットフォーム(Medium、dev.to など)で、Python の記事が数万本、Rust の記事が数千本の規模で存在する中、F*（F Star）の記事は事実上ゼロに近い水準にあります。

イスラエル企業(Check Point、Wiz、Cybereason、CyberArk などのサイバーセキュリティ企業)の技術ブログ記事で F*(F Star) を主題としたものも、筆者が web で確認できた範囲では見つかりませんでした。

暗号と形式検証の世界的な蓄積を持つイスラエルにおいてすら、F*（F Star）の技術者向け情報発信は、学術論文と公式リソースの領域を大きく越えていないというのが、2026年8月1日時点の実情です。

全体を俯瞰すると

F*（F Star）は、世界のセキュリティ・クリティカルな領域の研究・実務で確固とした存在感を築いています。

そのため、中国・ロシア・イスラエル・韓国・日本に加えて、定理証明・形式証明の歴史的な中心地である欧米ですら、F*（F Star）を主題とする記事が極めて乏しい現状にあっても、この言語が持つ将来性に期待をかけることができると考えています。

そうした認識に立ち、筆者は、日本語圏における認知度が低いいまこそ、敢えて、皆様の周囲のエンジニアやプログラマ、技術者の方々に先駆けて、皆様がこの言語を一足先に学び始めておくことは、将来、キャリア構築に際しての資産として回収可能性のある有望な先行投資になるのだと考えています。

F*（F Star）：AI Agent 時代の学習環境

これまでの繰り返しになる部分もありますが、筆者がF Star言語を学ぶべきだと考える根拠を改めて記載します。

（理由１）AI Agent 時代における形式検証の価値の高まり

筆者は、すでに公開済みのQiita記事 AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中するの中で、以下の主張を展開しました。

「AI Agent は、論理的に正しくとも社会規範に反したコードを、正しいと判断してしまう」

そして、別の記事形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界では、形式証明が保証できるのは「実装が仕様通りに動くこと」であり、「仕様が人間の意図を反映しているか」までは保証できないという論点を提示しました。

この２つの主張は、AI Agent 時代における形式検証の価値に光を当てるものです。AI Agentが生成したコードの正しさを機械的に検査し、証明できるF Starのような言語の価値を高めているのです。

（理由２）安全性が問われる” security-critical”な領域における実務的なニーズの高まり

F* は、既に暗号ライブラリ、通信プロトコル、電子投票、ブロックチェーンなど、安全性と信頼性が厳格に求められる領域（英語では、security-criticalという形容詞がこのような文脈で用いられます）で採用され、F*で記述されたコードが稼働しています。

この事実は、F* を学ぶことが、こうした領域におけるキャリアの構築に直結する可能性を示唆しています。

とりわけ、Web3、金融、医療、防衛、電力、通信 などの分野で、形式検証されたコードへの需要は、今後、さらに高まると考えられます。

（理由3）AI Agent との相性の良さ

F* は、AI Agent との相性が良い言語です。
理由は、次のとおりです。

（１）
F* は、SMT ソルバー(Z3)による証明の自動化を強力にサポートしており、AI Agent が証明の一部を自動生成することが容易である

（２）
F* の GitHub 公式リポジトリには、AI Agent での F* 使用を支援する記述 があること。

実際、「AI Agent は F* と Pulse を扱うことに習熟しつつあり、Copilot CLI や Claude Code を使う場合は、proof-copilot プラグインのインストールを推奨する」 と公式に記されています。
(出典 https://github.com/FStarLang/FStar)

（３）
AI Agent が生成したコードを、F* の形式検証で厳密に検査する ことで、AI Agent の生産性と、コードの正しさを両立できること。

どんなユースケースで威力を発揮するか

F* が特に威力を発揮するユースケースは、次のとおりです。

１. 暗号ライブラリの実装

HACL*、EverCrypt の実例が示すとおり、暗号アルゴリズムの実装は、F* が最も威力を発揮する領域の一つです。暗号のバグは致命的な脆弱性となるため、形式検証の負担を受け入れる価値があります。

２. 通信プロトコルの実装

miTLS-fstar、EverQuic-crypto の実例が示すとおり、TLS や QUIC などの通信プロトコルの実装も、F* が強い領域です。

３. バイナリ・パーサの実装

バイナリ・パーサとは、ネットワーク通信で送受信されるデータの並び(0 と 1 のビット列)を、プログラムが扱える意味のあるデータ構造へと変換する部品です。

皆様がWebブラウザでWebサイトを見るとき、皆様のブラウザは受信したデータを、バイナリ・パーサを通じて解釈しています。

バイナリ・パーサのバグは、しばしば重大なセキュリティ問題を引き起こします。

悪意ある入力を正しく検出できないと、バッファ・オーバーフローや任意コード実行といった深刻な脆弱性の温床となります。

F*（F Star）から派生した EverParse というツールは、バイナリ・データの仕様を記述するだけで、メモリ安全性と機能的正しさが証明済みの C 言語パーサを自動生成してくれます。

このツールが生成したパーサは、Microsoft Azure の仮想化基盤 Hyper-V の内部で、Azure クラウドを通過するすべてのネットワーク・パケットの解析と検証に使われています。

バイナリ・パーサの自動生成は、F(F Star) が実務で大きな価値を発揮する領域の一つ*です。

4. ブロックチェーンと Web3

ブロックチェーンとは、取引や資産の記録を、複数のコンピュータで分散して管理する仕組みで、暗号技術によって記録の改ざんを困難にします。

スマート・コントラクト(契約内容をコード化して自動実行する仕組み)を扱えるブロックチェーンも登場しており、その代表格の一つが Tezos です。

ブロックチェーンの正しさは、その内部で使われる暗号アルゴリズムの正しさに完全に依存します。

もし暗号にバグがあれば、資産の盗難や取引の改ざんが可能になってしまいます。

Tezos は、F*（F Star）から派生した HACL* という検証済み暗号ライブラリをその暗号プリミティブとして採用しています。

F*（F Star）で数学的に正しさが証明された暗号コードが、Tezos ブロックチェーン上で日々動いている取引の安全を裏付けているわけです。

ブロックチェーンや Web3 の分野で、暗号の正しさの証明を実務のシステムに組み込む取り組みは、F*(F Star) が既に踏み込んでいる領域の一つです。

5. 電子投票、選挙システム

電子投票とは、紙の投票用紙の代わりに、コンピュータやネットワークを使って投票を行い、集計する仕組みです。

電子投票のシステムの完全性(投票が改ざんされず、正しく集計されたことを検証できる性質)は、民主主義の根幹に関わる重要な要件です。

Microsoft が公開しているオープンソースの ElectionGuard は、電子投票の完全性を暗号技術で担保するための開発キット（SDK） です。

ElectionGuard の暗号処理には、F*（F Star）で数学的に正しさが証明された暗号コードが採用されています。

民主主義の根幹である選挙システムの完全性の検証にも、F*（F Star）が実務で使われています。

6. 暗号以外への広がり ── OS・コンパイラ・ブラウザ・WebAssembly・ファームウェア

ここまでの実例は暗号分野に偏って見えるかもしれませんが、F*（F Star）の適用範囲は、暗号だけにとどまりません。

OS・クラウド基盤 ── EverParse が生成した検証済みパーサは、Microsoft Azure の仮想化基盤 Hyper-V の内部で稼働しています
コンパイラ・低レベルコード生成 ── F* のコードを C 言語に変換する KaRaMeL や、アセンブリ・コードを検証する Vale といったツール群が、検証済みの低レベルコード生成を支えています
ブラウザ ── Mozilla Firefox の暗号ライブラリ NSS には、F* で検証された HACL* のコードが組み込まれています
WebAssembly ── HACL* は WebAssembly にもコンパイルされており、ブラウザ上で動く検証済み暗号として利用できます
ファームウェア ── デバイス起動時の完全性を守るセキュリティ・ファームウェア(DICE)を F* で検証した DICE* という成果も発表されています

Claude Code、Cursor、Kiro などの Agentic Coding 環境における F* サポート

Agentic Coding(AI Agent によるコーディング支援)環境における F* のサポート状況は、次のとおりです(2026年8月1日時点でweb で確認できた範囲での情報)。

Claude Code

F* GitHub 公式リポジトリで、Claude Code での F* 使用が明示的に推奨されており、proof-copilot プラグインのインストールが公式に案内されています。

Anthropic 社の Claude Code は、F* コミュニティが公式に推奨する Agentic Coding 環境の一つと位置付けられます。

GitHub Copilot CLI

F* GitHub 公式リポジトリで、Copilot CLI での F* 使用も明示的に推奨されており、同じく proof-copilot プラグインが案内されています。

Cursor、Kiro

CursorとKiro については、2026年7月末時点で、F* コミュニティによる公式の推奨や、専用のサポート・パッケージが公開されているかは、webで調べた範囲では明らかではありません。

ただし、Cursor は VS Code をベースにしており、F* は VS Code に対する公式サポートを提供しているため、Cursor から F* を使うことは技術的には可能と考えられます。

AI Agent との統合が進んでいる Claude Code と GitHub Copilot CLI は、F* を学ぶ皆様にとって、極めて有力な選択肢です。

学習リソース

F* を学ぶための主要なリソースを、次に整理します。

１.公式書籍「Proof-Oriented Programming In F*」

F* の主要開発者である Nikhil Swamy、Guido Martínez、Aseem Rastogi の3名による、公式のオンライン書籍です。

PDF版と、ブラウザ上で例題や演習を試せるTutorial版が、公式サイト(https://fstar-lang.org)から提供されています。

**２. F* 公式サイト**

https://fstar-lang.org が公式サイトです。ドキュメント、Tutorial、論文、コミュニティへのリンクがまとめられています。

**3. F* GitHub リポジトリ**

https://github.com/FStarLang/FStar が公式リポジトリです。ソースコード、Issue、Discussions を通じたコミュニティとの対話が可能です。

4. Zulip コミュニティ

F* コミュニティは Zulip というチャット・プラットフォームでの対話を推奨しています。開発者と直接やり取りできる貴重な場です。

F* を学ぶことは、少なくとも短期的には学習コストが高いです。

関数型プログラミング、依存型、篩型、SMT ソルバー、対話的定理証明、これらの概念を、順に身につける必要があります。

しかし、F* を学ぶことで、「AI Agent 時代における、機械が検証できる正しさとは何か」という実務と学問の両方で決定的に重要な問いに、正面から向き合うことができます。

その営みの中で、皆様のブラウザ Firefox で今この瞬間動いている HACL* のコードを、自分の目で読み、その正しさの証明を、自分の手で確かめられるようになるのです。

この経験は、実務のエンジニアとしての皆様の視座を、一段、確実に高めてくれるのではないでしょうか。

【対話篇】タロウくんと専任講師の対話 ──AI Agent 時代のF*（F Star）

ここからは、対話形式で「AI Agent 時代のF*(F Star) 」について考えてみたいと思います。

登場するのは、形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界
の登場人物、タロウくんと専任講師です。

タロウくん
先生、今日は F* について書かれた記事を一本読みました。

専任講師
感想を聞かせてくれるかな。

タロウくん
F* が、Firefox や Linux カーネルや WireGuard で動いている、というのが、いちばん驚きでした。

「証明された暗号コード」が、僕の日常のブラウザの中ですでに動いていることを初めて知りました。

専任講師
それは大きな発見だね。
君が見つけたFのユースケースは、F が単なる学術言語ではなく、私たちの日常生活を支える実用言語であることを雄弁に物語ってくれる好事例と言える。

タロウくん
そうなんです。

そして、F* が Claude Code や Copilot CLI での使用を公式に推奨している、というのも意外でした。

AI Agent と形式証明が、これほど近い場所で出会っているとは、思っていませんでした。

専任講師
その気付きは、極めて重要だ。

AI Agent がコードを生成する時代に、そのコードの正しさをどう保証するか。
その問いに対して、F* は、極めて明確な答えの一つを提示している。

タロウくん
先生、僕、F* を学ぼうと思います。

専任講師
うん、いい判断だ。
── ただ、一つだけ、覚えておいてほしいことがある。

F* が保証してくれるのは、「実装が仕様通りに動くこと」だ。

「その仕様が、本当に人間が望んでいたことを反映しているか」は、依然として人間が担うべき役割であり続ける。

形式手法と要求工学 ── この２本の柱の存在を忘れてはいけない。

タロウくん
その２本柱は、僕が読んだ記事の最後の締めくくりの段落で強調されていました。
胸にとどめておきたいとと思いました。

まとめ

F* は、Microsoft Research と INRIA の共同開発による「証明指向プログラミング言語」。関数型プログラミング、依存型、篩型、SMT ソルバーによる自動証明、対話的定理証明を統合した、極めて希少な言語です。
依存型と篩型のハイブリッドという設計により、書き手は場面に応じて、最適な道具を使い分けられます。単純な性質は篩型で自動証明、複雑な性質は依存型で厳密証明、という使い分けが可能です。
F* は 2011年に登場しました。Microsoft Research-INRIA Joint Centre(2005/2006年設立)の共同プロジェクトの一つとして、**「対話的定理証明系と汎用プログラミング言語のギャップを埋める」**ことを目標に開発されました。
F* の主要な用途は Project Everest。Mozilla Firefox、Linux カーネル、Tezos、ElectionGuard、WireGuard、mbedTLS などの実用システムで、F* で証明されたコードが動いています。
AI Agent 時代における F* の学習価値は、極めて高いと考えられます。F* GitHub 公式リポジトリは、Claude Code や GitHub Copilot CLI での F* 使用を推奨し、proof-copilot プラグインが用意されています。

F* を学ぶことは、AI Agent 時代のエンジニアの皆様にとって、「機械が検証できる正しさとは何か」という、実務と学問の両方で決定的に重要な問いに、正面から向き合うことです。この記事が、その第一歩の後押しになれば幸いです。

出典

F* 公式サイト https://fstar-lang.org
F* GitHub リポジトリ https://github.com/FStarLang/FStar
Project Everest 公式サイト https://project-everest.github.io/
Microsoft Research-INRIA Joint Centre https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/
Rocq(旧称 Coq)公式ドキュメント https://rocq-prover.org/doc/
Nikhil Swamy et al. "Secure Distributed Programming with Value-Dependent Types" ICFP 2011
Nikhil Swamy et al. "Dependent Types and Multi-Monadic Effects in F*" POPL 2016
Nikhil Swamy, Guido Martínez, Aseem Rastogi "Proof-Oriented Programming in F*" (2024)

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

F*（F Star）とは何か ── Firefox・Linux・WireGuard で動く「証明済みコード」を書けるプログラミング言語早わかり

はじめに

F*（F Star）はプログラミング言語の名前です

この記事を書く理由： 日本語圏における F*（F Star）の記事の少なさ

海外の状況： F*（F Star）の個人ブログ・企業技術記事の動静

（英語圏の状況）

（中国語圏の状況）

この状況が意味することは何か

中国の国家的関与の３つの層

３つの流れごとに、中国の国家的関与の姿

数学の形式化への関与

AI Agent × 定理証明への関与

セキュリティ・クリティカル・ソフトウェアの形式検証への関与

全体を俯瞰すると

韓国語圏、ロシア語圏、インド発の個人ブログの状況

全体を俯瞰すると

言語の名称表記について

F*（F Star）とはどんなプログラミング言語か

F*（F Star）の一次情報源

F*（F Star）と名前が似ている F#（F Sharp）との区別

想定読者

この記事を読む価値

TL;DR

F*（F Star）はどんな言語で、どんな立ち位置を築いているのか

８つの概念を整理する

１. 関数型プログラミング（ functional programming ）

２. 論理型プログラミング（ logic programming ）

3. 定理証明（ theorem proving ）

4. 形式検証（ formal verification ）

5. 依存型プログラミング（ dependent type programming ）

6. 篩型（ refinement types ）

7. SMT ソルバー（ SMT Solver 、Z3 ）

8. エフェクト（ monadic effects 、モナディック・エフェクト）

Tot： 純粋で必ず停止する関数

ML：副作用のある可能性がある関数

ST： 状態（参照）の読み書きを行う関数

Exn： 例外を発生させる可能性がある関数

Dv： 無限ループする可能性がある関数

F*（F Star）の立ち位置

Python では実現が難しい、F* の力が発揮される場面 ── 実務のユースケース

ユースケース１ ── 暗号ライブラリの実装

ユースケース２ ── バイナリ・パーサの生成

ユースケース３ ── TLS 1.3 の実装

F* のコード例

一言で言えば

F*（F Star）の限界 ── 他の定理証明・形式検証言語との役割分担

１. 数学そのものの形式化 ── Lean 4 の独壇場

２. 証明の対話的な組み立てと、タクティクの成熟度 ── Rocq・Isabelle の年輪

３. 証明の検査基盤の小ささ ── 「何を信頼するか」の違い

４. 最先端の型理論の探究 ── Agda と Cubical Agda

５. 大規模システム検証の金字塔 ── Isabelle と seL4

役割分担の全体像

使い分けの指針

依存型と篩型のハイブリッドという性格

依存型と篩型は、何が違うのか

F*は両者を統合した

タロウくんと専任講師の対話 ── 依存型と篩型のハイブリッド

F*（F Star）はどんな経緯で生まれたのか

INRIA と Rocq（旧称 Coq）── 定理証明系の歴史

Microsoft Research と INRIA の共同研究センター

なぜ Microsoft は F* をはじめとする定理証明・形式検証系の言語開発に取り組むのか

F* の生まれた経緯 ── 2011年、ICFP 論文

開発の動機は何だったのか

なぜ INRIA と Microsoft が組んだのか

目的は果たされたのか

現在も進化を続けている

F*（F Star）の用途と実際の利用実績

Project Everest ── F* の主要な用途

HACL* のコード実例 ── Firefox で動く暗号関数の型

2026年7月末時点までの世界各国での利用実績

１. Mozilla Firefox

２. Linux カーネル

３. Tezos ブロックチェーン

４. ElectionGuard 電子投票 SDK

５. WireGuard VPN

６. mbedTLS

INRIA/Microsoft が意図した用途との比較

全体を俯瞰する

我が国で F*（F Star）の認知度が低い理由と世界各国における存在感

日本での F*（F Star）の認知度が低い理由：筆者の見解

この記事を書く理由：日本語圏における F*（F Star）の記事の少なさ

**１. 関数型プログラミング（ functional programming ）**

**２. 論理型プログラミング（ logic programming ）**

**3. 定理証明（ theorem proving ）**

**4. 形式検証（ formal verification ）**

**5. 依存型プログラミング（ dependent type programming ）**

**6. 篩型（ refinement types ）**

**7. SMT ソルバー（ SMT Solver 、Z3 ）**

**8. エフェクト（ monadic effects 、モナディック・エフェクト）**

Tot：純粋で必ず停止する関数

ST：状態（参照）の読み書きを行う関数

Exn：例外を発生させる可能性がある関数

Dv：無限ループする可能性がある関数

**２. F* 公式サイト**

**3. F* GitHub リポジトリ**