A pure-Rust implementation of group operations on Ristretto and Curve25519

Verifying curve25519-dalek using Lean

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.

Rust interface for cvc5

Examples of efficiently using Apalache

Verus + Eris

Lean formalization of selected lemmas from "Term Rewriting and All That"

A set of cryptographic proofs for simple protocols, to be formalised in various tools.

A modal weakest precondition theory for the Iris program logic framework

A simple crater-inspired tool for Verus

Lean evaluation and metaprogramming utilities for provers.

Putnam 2025 formalized in Rocq

Logical relations for termination-insensitive noninterference in Iris

An MCP server for the fstar proof assistant

Auto formalization of the CLRS text book

Strong non-interference for fine-grained concurrent programs

Source code of http://certicrypt.gforge.inria.fr/certipriv/

Confidential Consortium Framework

Lean playground for programming language modeling tooling.

Shuttle is a library for testing concurrent Rust code

Extension of the Viper language with modular product programs and information flow specifications

List of bugs found in distributed protocols

A light-weight imperative language for developing provably privacy-preserving algorithms