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

F* is a general-purpose, proof-oriented programming language developed by Microsoft Research and Inria that combines dependent types with automated proof capabilities, compiling primarily to OCaml while also supporting extraction to F#, C, WebAssembly, and assembly. The open-source language, distributed under Apache 2.0, is designed for both functional and effectful programming and is actively maintained with binaries available for Windows, Linux, and macOS. F* is used in academic and industrial projects, including the high-assurance Project Everest for secure communication software.