F* (F*), pronounced "F star," is a general‑purpose proof‑oriented programming language that supports both purely functional and effectful code. It blends the expressive power of dependent types with proof automation via SMT solving and tactic‑based interactive theorem proving.

By default, F* programs compile to OCaml, but fragments can also be extracted to F#, C, or WebAssembly using the tool KaRaMeL, or to assembly via the Valetoolchain. F* is implemented in itself and bootstrapped with OCaml, released under Apache 2.0, and hosted on GitHub under active development by Microsoft Research, Inria, and community contributors.

The language is taught at seasonal schools and has extensive learning materials, including an online book "Proof‑oriented Programming in F*", a Low* tutorial, and lecture notes from events such as the Oregon Programming Language Summer School. Community support is available through GitHub Discussions, Zulip, and a mailing list.

F* is adopted in industry and academia. The umbrella project Project Everest delivers high‑assurance secure communication software, with offshoots like HACL*, Vale Crypt, and Ever Parse. Their code is used in Mozilla Firefox, the Linux kernel, Python, mbed TLS, Tezos, Election Guard, Wireguard, and Windows Hyper‑V.