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 中的说明从源码构建。所有分发渠道均由微软研究院、Inria 以及社区的 F* 开发团队维护。
学习资源
F* 的主要学习材料是一本名为《面向证明的 F* 编程》的在线书籍，辅以 Low* 教程以及季节性学校的各种课程材料。
《面向证明的 F* 编程》一书定期更新，可在 F* 网站上获取 PDF 版本。伴随教程页面提供快照和可在浏览器中尝试的练习。另一个教程涵盖 Low*，即通过 KaRaMeL 编译为 C 的 F* 低级子集。来自诸如俄勒冈编程语言夏季学校（2019、2021）、ECI 2019 和 EUTypes 夏季学校 2018 等活动的课程材料也在线发布，包含讲义、幻灯片和代码示例。
Low* 子集
Low* 是 F* 的一个低级子集，可通过 KaRaMeL 编译为 C，从而实现验证的系统编程。
Low* 将 F* 限制为适合系统代码的片段，提供对内存布局和内联汇编的直接控制，同时保留语言的依赖类型系统。用 Low* 编写的代码可以在 F* 中证明其正确性，然后提取为高效的 C，因而适用于开发经过验证的密码学原语、解析器和操作系统组件。
社区与支持
F* 社区使用 GitHub 讨论区、公开的 Zulip 论坛、低流量邮件列表以及每月的 PoP Up 研讨会进行交流和支持。
问题和公告在 GitHub 讨论区处理。公开的 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* 曲线25519 代码，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）、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）。近期工作在 F* 中形式化了 CBOR、CDDL 和 COSE，并在 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