F (pronunciado «F star») es un lenguaje de programación de propósito general orientado a la demostración formal, que combina programación puramente funcional y con efectos. Reúne el poder expresivo de los tipos dependientes con automatización de pruebas basada en resolutores SMT y demostración interactiva mediante tácticas. Por defecto, los programas en F se compilan a OCaml, y diversos fragmentos pueden extraerse a F#, C o WebAssembly con la herramienta KaRaMeL, o a ensamblador mediante la cadena de herramientas Vale. El propio compilador está implementado en F* y se arranca usando OCaml.
El proyecto es de código abierto bajo licencia Apache 2.0 y está disponible en GitHub, con binarios para Windows, Linux y macOS, además de instalación mediante OPAM, Docker y Nix. Su desarrollo lo impulsan Microsoft Research, Inria y la comunidad.
Entre sus usos industriales destaca Project Everest, que produce software de comunicaciones seguras de alta garantía. De él han surgido bibliotecas como HACL* (primitivas criptográficas verificadas, usadas en Mozilla Firefox, el kernel de Linux, Python, mbedTLS, la blockchain Tezos, ElectionGuard y Wireguard), EverCrypt (proveedor criptográfico unificado) y EverParse (generador de parsers binarios verificados, empleado en Windows Hyper-V para validar paquetes en Azure y en eBPF-for-Windows).
F cuenta con material didáctico, como el libro en línea «Proof-oriented Programming in F» y tutoriales sobre Low*, su subconjunto de bajo nivel compilable a C. También es objeto de investigación activa en lenguajes de programación y métodos formales, con publicaciones en PLDI, POPL e ICFP sobre mónadas de Dijkstra, lógicas de separación concurrentes (SteelCore, USSL, PulseCore) y verificación relacional.