FStarLang

GPU kernel verification with Pulse

Verified garbage collectors in Pulse

Formally verified cryptography library for Pulse/F*

F* nightly builds

A Proof-oriented Programming Language

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

Proof Annotation Language: inline Pulse annotations for C

Auto formalization of the CLRS text book

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

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