github.com/fstarlang/fstar ↗

About fstarlang/fstar

F* is a proof-oriented programming language designed to integrate program verification with practical software development. It enables developers to write code alongside formal proofs of correctness, leveraging dependent types and Dijkstra monads to reason about program behavior. The language is built on a foundation of SMT solvers and interactive theorem proving, allowing both automated and manual verification of properties.

The system supports multiple workflows for different use cases. By default, F* verifies code without executing it, but developers can extract verified code to OCaml or F# for execution. Additionally, specialized tooling like KaRaMeL enables extraction to C and WebAssembly for systems code, while Vale supports extraction to assembly for cryptographic and low-level implementations. This flexibility allows F* to be applied across domains from high-assurance libraries to performance-critical security-sensitive code.

The project includes comprehensive documentation through an online book titled "Proof-oriented Programming in F*", a detailed wiki, and community support via Slack and Zulip forums. Editor support is available across multiple platforms with the most mature integration in Emacs. F* is released under the Apache 2.0 license and actively maintains its codebase written primarily in OCaml and F#, welcoming community contributions through standard GitHub workflows.