Tillicum Containers Training Materials

A cryptographic framework for building collaborative applications over an untrusted server. Research prototype.

A generic JSON document store with sharing and synchronisation capabilities.

πfs - the data-free filesystem!

Learn Lean 4 by fixing 70 small exercises, one at a time

Use Signal without a smartphone!

End-to-end demos: real Rust → Aeneas → Lean → VCVio game-based cryptographic security proofs (no sorry; make verify gates the axioms)

Adler-32 verified twice: a comparative formal-verification case study using Lean+Aeneas and Verus, with both proofs sorry-free and verifying the same byte-at-a-time spec.

Formal Verification for Web3 — Lean 4 workshop code (OTP, RSA, Diffie-Hellman)

A Proof of RSA Encryption using Lean

A formally verified symbolic cryptography library for Lean

Deployments of fancy cryptography

LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.

Project to formally verify SPQR using Lean

Runtime monitoring of formal specifications

Verified implementation of the Open Vote Network protocol

Harden your Rust with specifications.

Cryptographic protocol analysis for real-world protocols.

Proving leftpad correct two-dozen different ways

Esoteric programming language based on emails

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.