A fuzzer for the MiniJava language

WebAppSec Subresource Integrity

The comprehensive guide for online anonymity and OpSec.

Explainers from Mozilla contributors

A Library for Representing Recursive and Impure Programs in Coq

Hybrid Public-Key Encryption

An implementation of an auditable key directory

Key Transparency Auditor for Signal

Specula: A Framework for Synthesizing High-Quality TLA+ Specifications from Source Code

A Pythonic framework for threat modeling

Starlit Jellyfish is a design for a verifiable map, a useful building block in a transparency system.

Artifact for the paper "A Generic Methodology for the Modular Verification of Security Protocol Implementations"

Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"

TypeScript implementation of a Sigsum verifier, for in-browser use.

An explainer to propose how the WebCrypto API can be extended to support Hardware Backed keys

Blowing the whistle through a news app

A framework for formally verifying distributed systems implementations in Coq

A language for symbolic transitions system, inspired by Ivy.

A tool for verifying game-hopping proofs

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

A set of examples of crypto implementations

This is the mechanization of the propositional fragment of Frege's Begriffsschrift and Duarte's independence proof using the Lean theorem prover.

SQLSync is a collaborative offline-first wrapper around SQLite. It is designed to synchronize web application state between users, devices, and the edge.

A draft proposal for the transparency mechanism for the W3C Web Application Integrity, Consistency, and Transparency spec

Pure Rust implementation of HPKE (https://www.rfc-editor.org/rfc/rfc9180.html)