William Schultz

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

tlaplus_animation. A TLA+ module for animating TLC traces.

tlaplus_repl. A simple REPL for TLA+.

endive. Tool for automatically inferring inductive invariants of distributed protocols.

mongo-repl-tla-models. TLC models for the MongoDB Replication TLA+ specification.

snapshot-isolation-spec. A formal specification of snapshot isolation.

logless-reconfig. TLA+ specifications and proofs of Logless Dynamic Reconfiguration in MongoDB Replication.

MP-69D-Scoreboard-Decoder. Arduino code and a Python script for decoding the data signal from the Fairplay MP-69D scoreboard controller unit.

scimitar. Verification tool for distributed protocols based on inductive proof decomposition.

initial-sync-tla. TLA+ specification of MongoDB replication initial sync.

endive-artifact. TLA

cbson_afl. BSON implementation in C with AFL Fuzzing Demo

mongo-repl-tla. TLA+ Specification of the MongoDB Replication Protocol

go_prng_cracker. Cracking Go's Default PRNG

Rietveld-Usability-Toolkit. Chrome extension to make Rietveld code review more usable. Customized a bit for MongoDB Code Review.

mongo-repl-reconfig. TLA+ spec of reconfiguration in MongoDB replication.

mypaxos. TLA

raft-by-refinement. Exploring refinement-based specification of the Raft consensus protocol.

reconfig-traces. TLA

mysat. C++

will62794.github.io. My personal website.

ocaml_chess. The classic game of chess, implemented in OCaml. Originally the final project for Cornell CS3110.