- F* is a proof-oriented programming language combining dependent types with SMT solving and tactic-based interactive theorem proving.
- It compiles by default to OCaml and can be extracted to F#, C, Wasm, or assembly using various tools.
- F* is open source under Apache 2.0, available on GitHub, and installable via multiple methods including binaries, OPAM, Docker, Nix, or from source.
- Learning resources include an online book, a Low* tutorial, and course materials from seasonal schools.