F*（发音为 F 星）是一种通用的面向证明的编程语言，支持纯函数式和带副作用的编程。它结合了依赖类型的表达能力以及基于 SMT 求解和基于战术的交互式定理证明的证明自动化。

F* 程序默认编译为 OCaml。F* 的各个片段也可以通过名为 KaRaMeL 的工具提取到 F#、C 或 Wasm，或者使用 Vale 工具链提取到汇编语言。F* 使用 F* 实现，并使用 OCaml 引导。

F* 是 GitHub 上的一个开源项目，并且由微软研究院、Inria 和社区积极开发。

**下载**

F* 在 Apache 2.0 许可证下发布。Windows、Linux 和 Mac OS X 的二进制文件定期发布在 GitHub 的发布页面上。您还可以从 OPAM、Docker、Nix 安装 F*，或者按照 INSTALL.md 中的说明从源代码构建它。

**学习 F***

在线书籍《F* 中的面向证明编程》正在编写中，并且定期在线发布更新。您可能希望在浏览器中点击下面的图片，尝试示例和练习的同时阅读它。

我们还有一个教程，涵盖了 Low*，它是 F* 的一个低级子集，可以通过 KaRaMeL 编译成 C。

**课程资料**

F* 课程经常在各种季节性学校教授。其中一些课程的讲座和课程材料也是有用的资源。

**社区**

请使用 GitHub 讨论来询问有关 F* 的问题，了解公告等。

尽管我们之前使用过 Slack 实例，但我们旨在将我们的在线社区整合到 Zulip 上的这个公开论坛上。

我们还有一个邮件列表，流量非常低。您可以在 fstar-mailing-list 订阅。

F* PoP Up 研讨会是面向所有用户和开发人员的会议。我们的目标是每月安排一次，尽管时间安排不固定——我们希望在那里见到你！

您还可以通过 [email protected] 联系 F* 的维护人员。

**用途**

F* 用于工业和学术环境中的多个项目。我们在这里列出了一些。如果您在您的项目中使用 F*，请告知 fstar-mailing-list。

**Project Everest**

Project Everest 是一个总项目，它使用 F* 开发高保证的安全通信软件。F* 的很大一部分开发都受到 Project Everest 所针对的场景的推动。Project Everest 的几个分支继续作为自己的项目，包括下面列出的一些。

**HACL*、ValeCrypt 和 EverCrypt**

HACL* 是一个高保证密码原语库，使用 F* 编写并提取到 C 中。ValeCrypt 在 Vale 中提供了经过形式化证明的密码原语实现，Vale 是一个嵌入在 F* 中的经过验证的汇编语言编程框架。EverCrypt 将它们组合成一个单一的加密提供程序。这些项目中的代码现在在多个项目中用于生产，包括 Mozilla Firefox、Linux 内核、Python、mbedTLS、Tezos 区块链、ElectionGuard 电子投票 SDK 和 Wireguard VPN。

**EverParse**

EverParse 是一个用于二进制格式的解析器生成器，它生成从形式化证明的 F* 中提取的 C 代码。EverParse 的解析器在多个项目中用于生产，包括 Windows Hyper-V，其中经过 Azure 云平台的每个网络数据包首先由 EverParse 生成的代码进行解析和验证。EverParse 也用于其他生产环境中，包括 ebpf-for-windows。

**研究**

F* 是研究的热门话题，在编程语言和形式化方法社区中，以及在安全和系统社区中从应用的角度来看。我们下面列出其中一些，这些论文的完整引用可以在此书目中找到。如果您希望将您的论文包含在此列表中，请联系 [email protected]。

**F* 及其 DSL 的设计**

**应用于安全和密码学的应用**

许多在安全和密码学中应用 F* 的论文可以在 Project Everest 书目中找到。我们在这里也提到了几个突出的例子，以及与 Project Everest 无关的其他应用。

**系统中的应用**

**解析中的应用**

**编程、程序证明和程序分析中的应用**

**AI 辅助编程**

**其他**

**关于旧版 F* 的论文**

第一篇介绍名为 F* 的系统的论文发表在 2011 年。尽管当前版本的 F* 在 2015 年进行了重新设计和实现，但为了完整起见，我们在这里包含了一些旧的论文。