cvc5 Free plan 8.7 Visit 
F*
fstar-lang.org
Spec sheet
- Purpose
- F* is a general-purpose proof-oriented programming language for purely functional and effectful programming.Read 11 Oct 2026 · fstar-lang.org
- License
- F* is distributed under the Apache 2.0 license.Read 11 Oct 2026 · fstar-lang.org
- Community support
- The project directs questions to GitHub Discussions and a public Zulip forum, and lists a low-traffic mailing list and maintainer contact email.Read 11 Oct 2026 · fstar-lang.org
- Compilation
- F* programs compile by default to OCaml, and fragments can also be extracted to F#, C, WebAssembly, or assembly using KaRaMeL or Vale.Read 11 Oct 2026 · fstar-lang.org
- Core team
- The listed core development team includes contributors affiliated with Microsoft Research in Redmond and Bangalore.Read 11 Oct 2026 · fstar-lang.org
- Development
- F* is open source on GitHub and is under active development by Microsoft Research, Inria, and the community.Read 11 Oct 2026 · fstar-lang.org
- Implementation
- F* is implemented in F* and bootstrapped using OCaml.Read 11 Oct 2026 · fstar-lang.org
- Installation
- The project offers binaries for Windows, Linux, and Mac OS X, and installation through OPAM, Docker, Nix, or source builds.Read 11 Oct 2026 · fstar-lang.org
- Learning
- The site links to an online book, browser examples and exercises, and a tutorial for Low*, a low-level subset that can compile to C through KaRaMeL.Read 11 Oct 2026 · fstar-lang.org
- Parser tooling
- EverParse generates C code from formally proven F* and is used in production, including in Windows Hyper-V.Read 11 Oct 2026 · fstar-lang.org
- Production use
- The site says code from HACL*, ValeCrypt, and EverCrypt is used in production projects including Firefox, the Linux kernel, Python, mbedTLS, and WireGuard.Read 11 Oct 2026 · fstar-lang.org
- Proof system
- It combines dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving.Read 11 Oct 2026 · fstar-lang.org
- Security use
- Project Everest develops high-assurance secure communication software in F*, and HACL* provides high-assurance cryptographic primitives written in F* and extracted to C.Read 11 Oct 2026 · fstar-lang.org
Plans and prices
F* Free Apache 2.0 licensed · binaries for Windows, Linux, and Mac OS X · install via OPAM, Docker, or Nix, or build from source Read 11 Oct 2026 · fstar-lang.org
Where Specifiction places it
- Formal Verification Tools#11 of 348.0
