F*：让代码证明自身安全的编程语言

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

F* 是一款面向证明的通用编程语言，由 Microsoft Research 和 Inria 等机构联合开发。它巧妙结合了依赖类型的表达力与基于 SMT 求解的自动化证明能力，支持纯函数式与效应式编程。F* 程序默认编译为 OCaml，也可通过 KaRaMeL 提取为 C、Wasm 或 F#，甚至利用 Vale 工具链生成汇编代码。从 Mozilla Firefox 到 Linux 内核，再到 Tezos 区块链和 Wireguard VPN，F* 已广泛应用于高保障密码学库 HACL* 和 EverCrypt 等关键基础设施中。无论是验证低层代码的安全性，还是构建形式化验证的解析器 EverParse，F* 都在推动软件正确性的边界。