FStarLang

A Proof-oriented Programming Language

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

GPU kernel verification with Pulse

Proof Annotation Language: inline Pulse annotations for C

Formally verified cryptography library for Pulse/F*

Verified garbage collectors in Pulse

F* nightly builds

Auto formalization of the CLRS text book

A verified implementation of TLS in Pulse, programmed and verified by agents

A tree-sitter grammar for FStar and Pulse, with NodeJS and Rust bindings