F*: A general-purpose proof-oriented programming language

F*：一种通用的面向证明的编程语言

F* (pronounced F star) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. F*（发音为 F star）是一种通用的面向证明的编程语言，支持纯函数式编程和带有副作用的编程。它结合了依赖类型的表达能力，以及基于 SMT 求解器和基于策略的交互式定理证明的自动化证明功能。

F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or Wasm by a tool called KaRaMeL, or to assembly using the Vale toolchain. F* is implemented in F* and bootstrapped using OCaml. F* is open source on GitHub and is under active development by Microsoft Research, Inria, and by the community. F* 程序默认编译为 OCaml。F* 的不同片段也可以通过名为 KaRaMeL 的工具提取为 F#、C 或 Wasm，或者使用 Vale 工具链提取为汇编语言。F* 本身由 F* 实现，并使用 OCaml 进行自举。F* 在 GitHub 上开源，目前正由微软研究院 (Microsoft Research)、法国国家信息与自动化研究所 (Inria) 以及社区共同积极开发。

Download

下载

F* is distributed under the Apache 2.0 license. Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub. You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in INSTALL.md. F* 基于 Apache 2.0 许可证发布。Windows、Linux 和 Mac OS X 的二进制文件会定期发布在 GitHub 的发布页面上。您也可以通过 OPAM、Docker、Nix 安装 F*，或者按照 INSTALL.md 中的说明从源代码构建。

Learn F*

学习 F*

An online book Proof-oriented Programming In F* is being written and regular updates are posted online. You probably want to read it while trying out examples and exercises in your browser by clicking the image below. 一本名为《Proof-oriented Programming In F*》（F* 中的面向证明编程）的在线书籍正在编写中，并会定期在线更新。您可以在阅读本书的同时，通过点击下方的图片，在浏览器中尝试其中的示例和练习。

Low*

We also have a tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL. 我们还提供了一份关于 Low* 的教程，Low* 是 F* 的一个底层子集，可以通过 KaRaMeL 编译为 C 语言。

Course Material

课程资料

F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are also a useful resource. F* 课程经常在各种季节性学校（暑期学校等）中教授。其中一些课程的讲座和资料也是非常有用的资源。

Community

社区

Please use GitHub Discussions to ask questions about F*, learn about announcements, etc. Although we previously used a Slack instance, we aim to consolidate our online community on this public forum on Zulip. We also have a mailing list, which has very low traffic. You can subscribe at fstar-mailing-list. 请使用 GitHub Discussions 来提问关于 F* 的问题、了解公告等。虽然我们之前使用过 Slack，但我们目前旨在将在线社区整合到 Zulip 的公共论坛上。我们还有一个邮件列表，流量非常低。您可以在 fstar-mailing-list 订阅。

The F* PoP Up Seminar, a users and developers meeting is open to all. We aim to schedule it once a month, though the schedule is irregular---we hope to see you there! You can also contact the maintainers of F* at fstar-maintainers@googlegroups.com. F* PoP Up 研讨会是一个面向所有人的用户和开发者会议。我们计划每月举办一次，尽管时间安排不固定——我们期待在那里见到您！您也可以通过 fstar-maintainers@googlegroups.com 联系 F* 的维护者。

Uses

用途

F* is used in several projects in both industrial and academic settings. We list a few of them here. If you are using F* in your project, please let us know by writing to the fstar-mailing-list. F* 被应用于工业界和学术界的多个项目中。我们在此列出其中一部分。如果您正在您的项目中使用 F*，请通过 fstar-mailing-list 写信告知我们。

Project Everest

Everest 项目

Project Everest is an umbrella project that develops high-assurance secure communication software in F*. A big part of the development of F* has been motivated by the scenarios that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including some of those listed below. Everest 项目是一个伞形项目，旨在用 F* 开发高保证的安全通信软件。F* 的很大一部分开发工作都是由 Everest 项目所针对的场景驱动的。Everest 项目衍生出了多个独立项目，包括下面列出的一些项目。

HACL*, ValeCrypt, and EverCrypt

HACL*、ValeCrypt 和 EverCrypt

HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C. ValeCrypt provides formally proven implementations of cryptographic primitives in Vale, a framework for verified assembly language programming embedded in F*. EverCrypt combines them into a single cryptographic provider. HACL* 是一个高保证加密原语库，用 F* 编写并提取为 C 语言。ValeCrypt 在 Vale 中提供了经过形式化验证的加密原语实现，Vale 是一个嵌入在 F* 中的验证汇编语言编程框架。EverCrypt 将它们组合成一个统一的加密提供程序。

Code from these projects is now used in production in several projects, including Mozilla Firefox, the Linux kernel, Python, mbedTLS, the Tezos blockchain, the ElectionGuard electronic voting SDK, and the Wireguard VPN. 来自这些项目的代码目前已被多个项目用于生产环境，包括 Mozilla Firefox、Linux 内核、Python、mbedTLS、Tezos 区块链、ElectionGuard 电子投票 SDK 以及 Wireguard VPN。

EverParse

EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*. Parsers from EverParse are used in production in several projects, including in Windows Hyper-V, where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other production settings, including ebpf-for-windows. EverParse 是一个二进制格式解析器生成器，它生成的 C 代码是从经过形式化验证的 F* 中提取出来的。EverParse 生成的解析器已被多个项目用于生产环境，包括 Windows Hyper-V，其中通过 Azure 云平台的每个网络数据包都会首先由 EverParse 生成的代码进行解析和验证。EverParse 也被用于其他生产环境，包括 ebpf-for-windows。

Research

研究

F* is an active topic of research, both in the programming languages and formal methods community, as well as from an application perspective in the security and systems communities. We list a few of them below, with full citations to these papers available in this bibliography. If you would like your paper included in this list, please contact fstar-maintainers@googlegroups.com. F* 是编程语言和形式化方法社区的一个活跃研究课题，同时在安全和系统社区的应用层面也备受关注。我们在下方列出了一些研究，这些论文的完整引用可在该参考文献列表中找到。如果您希望将您的论文加入此列表，请联系 fstar-maintainers@googlegroups.com。

(Note: The list of research papers follows the same pattern of title and description; for brevity, the translation continues with the provided structure.)

The Design of F and its DSLs* F 及其 DSL 的设计*

Dependent Types and Multi-monadic Effects in F (POPL 2016)**: This is the canonical reference describing the F system. The language has evolved in significant ways since 2016, however, its core design and implementation is based on this paper. F 中的依赖类型与多单子副作用 (POPL 2016)**：这是描述 F 系统的权威参考资料。自 2016 年以来，该语言已经发生了重大演变，但其核心设计和实现仍基于这篇论文。
Verified Low-level Programming Embedded in F (ICFP 2017)**: which describes the Low fragment of F* which is a low-level subset of F* that can be compiled to C by KaRaMeL. 嵌入在 F 中的经过验证的底层编程 (ICFP 2017)**：描述了 F 的 Low* 片段，这是 F* 的一个底层子集，可以通过 KaRaMeL 编译为 C 语言。
A Verified, Efficient Embedding of a Verifiable Assembly Language (POPL 2019): which describes the Vale language, a verified assembly language embedded in F*. 一种经过验证的、高效的可验证汇编语言嵌入 (POPL 2019)：描述了 Vale 语言，这是一种嵌入在 F* 中的经过验证的汇编语言。
Meta-F: Proof Automation with SMT, Tactics, and Metaprograms (ESOP 2019)**: which describes MetaF, a metaprogramming system within F* used to implement various aspects of F*, ranging from its tactic engine to its support for typeclasses. Meta-F：利用 SMT、策略和元程序进行自动化证明 (ESOP 2019)**：描述了 MetaF，这是一个 F* 内部的元编程系统，用于实现 F* 的各个方面，从策略引擎到对类型类的支持。
Programming and Proving with Indexed Effects (TR 2021): which describes the design of F*‘s support for user-defined effects and provides a calculus that describes the logical core of F*. 使用索引副作用进行编程与证明 (TR 2021)：描述了 F* 对用户自定义副作用的支持设计，并提供了一个描述 F* 逻辑核心的演算系统。
Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (ICFP 2021): which describes the Steel language and its use of the SteelCore concurrent separation logic for proofs of imperative programs with various forms of concurrency. Steel：依赖类型并发分离逻辑中的面向证明编程 (ICFP 2021)：描述了 Steel 语言及其对 SteelCore 并发分离逻辑的使用，用于证明具有各种并发形式的命令式程序。

Semantics and Effects 语义与副作用

Verifying Higher-order Programs with the Dijkstra Monad (PLDI 2013): which introduces the concept of the Dijkstra monad, a core feature of F*‘s system of effects. 使用 Dijkstra 单子验证高阶程序 (PLDI 2013)：介绍了 Dijkstra 单子的概念，这是 F* 副作用系统的核心特性。
Dijkstra Monads for Free (POPL 2017): which shows how to automatical… 免费的 Dijkstra 单子 (POPL 2017)：展示了如何自动地……