微软开源验证语言 F*：支持自动化证明的高安全性编程环境

F*（发音 F star）是由微软研究院和 Inria 共同开发的一款通用“面向证明”的编程语言。该语言的核心特性在于融合了依赖类型的数学表达能力与高度自动化的证明机制，允许开发者在编写代码的同时，利用 SMT（可满足性模理论）求解器和交互式定理证明策略来自动化验证程序的正确性。F* 既支持纯函数式编程，也支持带副作用的编程模式，其默认编译目标是 OCaml。为了适应不同层级的开发需求，F* 生态系统包含了多个后端工具：KaRaMeL 可将代码提取为 F#、C 语言或 WebAssembly，而 Vale 工具链则支持将其编译为底层汇编语言，这种能力使得从高层算法到底层硬件实现的全链路验证成为可能。作为著名的 Project Everest 项目的核心组件，F* 曾被用于开发经过数学严格验证的 HTTPS 协议栈，以消除内存安全漏洞等高危风险。F* 编译器自身也是用 F* 编写并实现自举的，目前该项目已作为开源项目在 GitHub 上发布，由科研机构与社区共同维护。

事件分析

💡 核心观点：F* 通过代码自证机制将形式化验证工程化，为构建零漏洞的自动驾驶与芯片底层系统提供了工业级解决方案。