(at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4

universal composability in model checkers

Firefox user.js for optimal privacy and security. Your favorite browser, but better.

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

A huge blocklist of manually curated sites that contain AI generated imagery for uBlock Origin & uBlacklist.

Export any Kindle book you own as text, PDF, EPUB, or as a custom, AI-narrated audiobook. 🔥

Coq code formatter

Verifying concurrent storage and distributed systems

The TLA⁺ Proof Manager

A high-performance, zero-overhead, extensible Python compiler with built-in NumPy support

A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.

An Arbitrary Waveform Generator

A project of short tutorials and how-to guides for Coq features and Coq Platform packages.

Finite probability theory in Coq

Material for the course CAS CS 491: Type Theory and Mechanized Reasoning (Spring 2024)

A simple and elegant Jekyll theme for an academic personal homepage

Rewrites TLA⁺ specs to use Unicode symbols instead of ASCII, and vice-versa

Interactive playground for exploring and sharing TLA+ specifications in the browser.

Apollo for Reddit tweak with in-app configurable API keys

Tool for automatically inferring inductive invariants of distributed protocols.

Some unstructured notes concerning the Broad tutorial to take place in March 2020

Examples for EasyCrypt Lectures

text and image to video generation: CogVideoX (2024) and CogVideo (ICLR 2023)

Audio super resolution using neural networks