The Pulse separation logic DSL for F*

Linux device manager for Logitech devices

The Z3 Theorem Prover

HACL*, a formally verified cryptographic library written in F*

Lean formalization for the paper "Symbolic Automata: 𝜔-Regularity Modulo Theories"

neovim plugin for F*

A verification toolchain for Rust programs

A verified Merkle Tree, built as a standalone project on top of EverCrypt

A Proof-oriented Programming Language

Automated generation of provably secure, zero-copy parsers from format specifications

An interactive mode for F* in VS Code

Verified implementations for the Noise family of protocols

Verified implementation of TLS 1.3 in F*

Armada is a tool for writing, and proving correct, high-performance concurrent programs.

Waldo library for proving indistinguishability properties in F*

Native messenger for Tridactyl, a vim-like web-extension.

Security model and verified implementation of QUIC packet encryption in Low*, built over EverCrypt and EverParse.

Lean 4 programming language and theorem prover

🎮 ⌨ An easy to use tool to change the behaviour of your input devices.

White-box automation for Lean 4

Nix Packages collection

Lean 4 build system and package manager with configuration files written in Lean.