Stars
Trusted Timestamping Framework for Scientific Research
Natural language tactics to teach mathematics using Lean 4
A collection of formalized statements of conjectures in Lean.
🎲 A Distributed Randomness Beacon Daemon - Go implementation
Self describing hashes - for future proofing
Formal verification of a session data exchange protocol (SDEP) across Cryptol spec, SAW Hoare-logic proofs of C++/Rust implementations
Guidelines for Writing Cryptography Specifications
A project to map out the relations between different equational theories of Magmas.
A model checker for implementing distributed systems.
Foundational Cryptography Framework for machine-checked proofs of cryptography.
A tool for creating and managing Mailbags, a package for preserving email using multiple preservation formats
A high-level Rust library to help write clients for the Signal Messenger.
Lean/VCVio specifications and proofs for secure messaging protocols
[work in progress] Software for helping cryptographers manage game-hopping proofs in LaTeX
A cryptographic framework for building collaborative applications over an untrusted server. Research prototype.
A generic JSON document store with sharing and synchronisation capabilities.
Learn Lean 4 by fixing 70 small exercises, one at a time
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.