← All repos

FStar

A Proof-oriented Programming Language

GitHubfstar-lang.org
c-languagedependent-typesdijkstra-monadsf-sharpfstarinteractive-theorem-provingocamlprogramming-languageprogram-proofproof-assistantsmttheorem-provingverification
Browse cluster: Lean4 Formal Verification & Cryptography →
48,823commits
194contributors
17languages

Tech stack & purpose

F* is a proof-oriented programming language designed for program verification and formal methods. Built on dependent types, SMT solvers, and theorem-proving capabilities, it enables developers to write code alongside machine-checked proofs of correctness. The language is implemented in OCaml and F#, with code extraction to OCaml, F#, C, and Rust, supported by complementary tools like KaRaMeL for C/Rust extraction and Vale for assembly. F* is developed by FStarLang, an active open-source community, and includes Pulse, a separation logic DSL for concurrent imperative programming, alongside comprehensive documentation in the form of an online book and editor support for Emacs and VS Code.

Community & reference links

Languages

F*
91.7%
OCaml
3.3%
Makefile
1.0%
Rust
1.0%
Python
0.8%
Shell
0.8%
C
0.8%
F#
0.3%
Dockerfile
0.1%
Jupyter Notebook
0.0%
Nix
0.0%
Rocq Prover
0.0%
Haskell
0.0%
Dune
0.0%
Gnuplot
0.0%
Standard ML
0.0%
Emacs Lisp
0.0%

Contributors (top 30 of 194)