A Proof-oriented Programming Language

Verified garbage collectors in Pulse

F* nightly builds

An LSP server for SMT-LIB files, with a VS Code extension for syntax highlighting and language support.

KaRaMeL is a tool for extracting low-level F* programs to readable C code

Proof Annotation Language: inline Pulse annotations for C

A Copilot-CLI Plugin for F* and Related Tools

The website of all things F*

Auto formalization of the CLRS text book

The Steel separation logic library for F*