F* (pronounced F star) is a general-purpose, proof-oriented programming language designed for writing programs together with machine-checked proofs of their properties.
It combines dependent types with automated and interactive theorem proving. F* supports purely functional and effectful programming, using SMT solving, symbolic computation, and tactics to discharge proof obligations. Verified programs can be extracted to languages including OCaml and F#, while specialised toolchains support C, Rust, WebAssembly, and assembly output.
This is free and open source software.
Key Features
- Dependent and refinement types for expressing precise program properties.
- Supports both purely functional and effectful programming.
- Automates proofs using SMT solving and symbolic computation.
- Offers tactic-based interactive theorem proving.
- Supports user-defined computational effects.
- Combines programming and proofs in a single language.
- Extracts verified code to OCaml and F#.
- Supports low-level verified programming through Low* and KaRaMeL.
- Provides specialised routes for generating C, Rust, WebAssembly, and assembly code.
- Offers interactive development support for Emacs and Visual Studio Code.
Website: github.com/FStarLang/fstar
Support:
Developer: F* developers
License: Apache License 2.0
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |