TLA+ and Alloy specs of database isolation

A collection of "git for data" snippets, models, resources

MongoDB Adaptation of PyTPCC

📝 Web-based, reactive Datalog notebooks for data analysis and visualization

A Python-like programming language for testing and experimenting with concurrent programs.

🔬 A fast, interactive web-based viewer for performance profiles.

A bidirectional manipulation editor for diagramming

RocksDB/LevelDB inspired key-value database in Go

Pushshift API

Drive a browser with GPT-3

Access large language models from the command-line

Formal specification of PBFT in TLA+

TLA+ specifications accompanying paper: Automated Validation of State-Based Client-Centric Isolation with TLA+. (https://doi.org/10.1007/978-3-030-67220-1_4) Based on Crooks' Isolation (https://dl.…

IPA(Interaction-Preserving Abstraction) is a framework that leverages characteristics of TLA+ and enables practical and efficient compositional model checking for TLA+ specifications of distributed…

Sonoma Aerials Downloader

A natural language interface for computers

The TLA⁺ Proof Manager

TLA+ specification of Fast Flexible Paxos

Collection of Distributed Protocol Verification Problems

A Swiss Army knife for read-write quorum systems

TLA+ description for the CAS-Paxos algorithm

This repository contains the TLA+ specification of the 1-Update cache coherence protocol that appeared in PACT'21.

Solution to the subset sum problem via a heap-ordered tree structure consisting of n-length subsets of a set

Responsive, animated figures in JavaScript/HTML canvases

Early-stage research project to analyze the dependency structure of invariants generated by IC3/PDR.

TLA+ formalization of a distributed termination-detection algorithm, including a proof checked with Apalache