引言 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 的发布页面上。您也可以通过按照 INSTALL.md 中的说明从 OPAM、Docker、Nix 安装 F*，或者从源代码构建。学习 F* 一本关于 F* 的在线书籍《面向证明的编程》正在撰写中，并定期在线更新。您可能想在通过点击下图在浏览器中尝试示例和练习的同时阅读它。Low* 我们还有一个教程，涵盖 Low*，F* 的一个低级子集，可以由 KaRaMeL 编译为 C。课程材料 F* 课程通常在各种季节学校中教授。其中一些讲座和课程材料也是有用的资源。嵌入 F* 中的面向证明的编程语言 线上讲座在俄勒冈编程语言夏季学校（2021）：讲义、幻灯片、代码 使用 F* 和 Meta-F* 的形式化验证 讲座和教程在 ECI 2019：讲义、幻灯片、代码 验证低级代码的正确性和安全性 讲座在俄勒冈编程语言夏季学校（2019）：讲义、幻灯片、代码 使用 F* 的程序验证 2018 年 EUTypes 夏季学校课程，2018 年 8 月 8-12 日，马其顿奥赫里德课程材料 社区 请使用 GitHub Discussions 提问与 F* 相关的问题，了解公告等。尽管我们以前使用过 Slack 实例，但我们希望在这个公共论坛 Zulip 上整合我们的在线社区。我们还有一个邮件列表，流量非常低。您可以在 fstar-mailing-list 订阅。F* PoP Up 研讨会，用户和开发者的会议对所有人开放。我们希望每月安排一次，尽管 schedule 不规律——希望能在那时见到您！您还可以通过邮件与 F* 的维护者联系，邮件地址是 fstar-maintainers@googlegroups.com。用途 F* 在多个工业和学术项目中使用。我们在这里列出了一些。如果您在项目中使用 F*，请通过向 fstar-mailing-list 写信告诉我们。项目 Everest 项目 Everest 是一个发展高保证安全通信软件的伞形项目，使用 F* 编写。F* 的开发很大一部分是受到项目 Everest 所针对场景的激励。项目 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* 是编程语言和形式方法社区的一个活跃研究主题，同时在安全和系统社区的应用视角方面也很有研究价值。我们在下面列出了一些研究论文，并在此书目中提供了完整引用。如果您希望将您的论文纳入此列表，请联系 fstar-maintainers@googlegroups.com。F* 及其 DSL 的设计 依赖类型和 F* 中的多单子效果（POPL 2016） 这是描述 F* 系统的权威参考。然而，自 2016 年以来，该语言在多个方面发生了显著演变，但其核心设计和实现基于这篇论文。嵌入在 F* 中的经过验证的低级编程（ICFP 2017），描述 F* 的 Low* 片段，这是一个可以由 KaRaMeL 编译为 C 的 F* 的低级子集。经过验证的高效嵌入可验证的汇编语言（POPL 2019），描述了 Vale 语言，一个经过验证的汇编语言。