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 程式語言夏季學校（2019、2021）、ECI 2019 及 EUTypes 夏季學校 2018，亦有線上發布，內含講義、投影片與程式碼範例。
Low* 子集
Low* 是一個可經由 KaRaMeL 編譯為 C 的 F* 低階子集，使得驗證系統程式設計成為可能。
Low* 將 F* 限制為適合系統程式碼的片段，提供對記憶體佈局的直接控制以及內嵌組合語言，同時保留語言的依賴類型系統。以 Low* 編寫的程式碼可在 F* 中證明其正確性，然後提取為高效率的 C 程式碼，適合用於開發已驗證的密碼學原始程式、解析器及作業系統元件。
社群與支援
F* 社群透過 GitHub Discussions、公開的 Zulip 論壇、低流量郵遞清單以及每月一次的 PoP Up 講座進行溝通與支援。
問題與公告會在 GitHub Discussions 論壇中處理。公開的 Zulip 聊天室（fstar.zulipchat.com）作為主要即時討論場所。Google Groups 郵遞清單存在於低流量公告。F* PoP Up 講座是一個使用者與開發者會議，雖然舉辦時間不固定，但目標是每月一次。維護者可透過 fstar-maintainers@googlegroups.com 聯繫。
工業與學術應用
F* 在數個高保證項目中被使用，最著名的是 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 的密碼學庫納入 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》，描述 metaprogramming 系統。其他論文涵蓋 Dijkstra monads、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）、Pipit 用於反應式即時系統（ECOOP 2024）以及 StarMalloc，一個經 Steel 驗證的硬化併發記憶體分配器（SPLASH 2024）。
在解析上的應用
F* 推動了已驗證的解析器生成器，如 EverParse 與 ASN1*，它們能產出對 CBOR、CDDL、COSE 及 ASN.1 DER 等二進位格式的正確 C 解析器。
EverParse 首次出現在 USENIX Security 2019，後來被用於堅固 Hyper‑V 封包解析器（PLDI 2022）。ASN1* 提供已驗證的 ASN.1 DER 解析（CPP 2022）。近期工作將 CBOR、CDDL 與 COSE 形式化於 F*，並透過 Pulse（CCS 2025）開發出可驗證正確的解析器與格式化器。
在程式設計、程式證明與程式分析上的應用
F* 支援可逆電路、工作階段類型多方協議、抽象解譯器、法律專用語言的編譯，以及 Rust 與 OCaml 程式碼的驗證。
顯著成果包括可逆電路的驗證編譯器（CAV 2018）、Session* 用於多方協議（OOPSLA 2020）、在 F* 中驗證的抽象解譯框架（SAS 2021）、Catala 語言（適用於法律，含已驗證編譯器部分）（ICFP 2021）、梅克爾帕特裡樹的驗證（arXiv 2021）、Aeneas 將 Rust 轉譯至 F* 以達功能正確性（ICFP 2022）、Q* 調整 SteelCore 以適用於量子分離邏輯（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