F是一种通用的面向证明编程语言，由Microsoft Research、Inria和社区共同开发，以Apache 2.0许可证开源[1]。该语言结合了依赖类型的表达力与基于SMT求解的证明自动化功能，支持纯函数式和有副作用的编程[1]。F程序默认编译为OCaml，可通过KaRaMeL工具提取到F#、C或Wasm，通过Vale工具链提取到汇编[1]。
F已在多个生产环境中获得广泛应用。密码学库HACL、ValeCrypt和EverCrypt的代码目前被Mozilla Firefox、Linux内核、Python、mbedTLS、Tezos区块链和WireGuard VPN等项目使用[1]。二进制格式解析器EverParse被集成到Windows Hyper-V中，用于处理通过Azure云平台的网络数据包[1]。
F* is a programming language designed to combine expressive dependent types with automated proof capabilities, developed collaboratively by Microsoft Research, Inria, and the community.[1] The language supports both pure functional and side-effecting programming paradigms, with programs compiling to multiple targets including OCaml, F#, C, WebAssembly, and assembly code.[1] Released under the Apache 2.0 license, F* leverages SMT solver-based automation to assist developers in formal verification.[1]
The language has achieved significant real-world deployment across security-critical systems and applications.[1] Major projects built on F* include Project Everest for high-assurance secure communication, HACL* for cryptographic primitives, and EverParse for binary format parsing.[1] Code generated from HACL*, ValeCrypt, and EverCrypt libraries now runs in production environments spanning Mozilla Firefox, the Linux kernel, Python, mbedTLS, the Tezos blockchain, and WireGuard VPN.[1] Additionally, EverParse processes network data packets flowing through Windows Hyper-V in Azure cloud infrastructure.[1]