Lists (27)
💻 algorithms
5 repositories
📚 Books
10 repositories
C/CPP
17 repositories
Code Reading
6 repositories
💻 Compilers
36 repositories
💻 Computer Systems
3 repositories
💯 Coq
6 repositories
🪜 Courses
9 repositories
💻 Databases
23 repositories
Distributed Computing
1 repository
Formal Methods
25 repositories
🔮 Future ideas
1 repository
🏪 gallery
1 repository
✨ Inspiration
Java
1 repository
LaTeX-TikZ-PGFPlots
1 repository
📖 Libraries
1 repository
🧰 LLM
19 repositories
LLVM
3 repositories
ML
Machine Learning9 repositories
My Projects
1 repository
🚀 My stack
Paper-List
2 repositories
Research
33 repositories
RISC-V
4 repositories
TLA+
11 repositories
Tools
1 repository
Starred repositories
34
stars
written in TLA
Clear filter
A collection of TLA⁺ specifications of varying complexities.
writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+
Dr. TLA+ series - learn an algorithm and protocol, study a specification
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!
TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
PGo is a source to source compiler from Modular PlusCal specs into Go programs.
A TLA+ specification of the Apache BookKeeper replication protocol
TLA+ specification of the Kafka replication protocol
Distributed termination detection on a ring, due to Shmuel Safra:
Reading the linearizability paper with TLA+
An instructional website with progressively worked examples of TLA+ specifications and model checking.
Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
Synchronous fault-tolerant distributed algorithms encoded in TLA+
Different TLA+ specifications, mostly for learning purposes
Tool for automatically inferring inductive invariants of distributed protocols.
Collection of Distributed Protocol Verification Problems
TLA+ specifications and proofs of Logless Dynamic Reconfiguration in MongoDB Replication.
Artifact package accompanying our POPL 2024 submission titled "A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability".
Verification tool for distributed protocols based on inductive proof decomposition.
Specification of the consensus algorithm in Tencent storage system PaxosStore
TLA+ model of Zookeeper's Atomic Broadcast protocol (Zab)
A collection of various standards, proposed or established, related to TLA+
TLA+ specifications for Open Network Operating System (ONOS)