Anvil is an experimental framework to build practical, formally verified, cluster management controllers.

Automatic Reliability Testing for Kubernetes Controllers and Operators

A static site generator for blogs.

PaxosStore has been deployed in WeChat production for more than two years, providing storage services for the core businesses of WeChat backend. Now PaxosStore is running on thousands of machines, …

Specification of the consensus algorithm in Tencent storage system PaxosStore

TLA+ specifications for Kafka related algorithms

A modular game engine written in Rust

Source code for the book Rust in Action

A non-offical LaTeX template used in NJU

Two-phase (2PC) and three-phase (3PC) protocols implementaion in Golang

A basic hotel reservation system with 2PC using pessimistic and optimistic locks in Go

A consensus that unifies paxos, raft, 2pc, etc.

Implementation of Two Phase Commit

A two-phase-commit protocol for leveldb.

Distributed Transaction Service For Spring Cloud

kiteq-common provides basic components for kiteq

两阶段提交协议的demo实现，主要用于个人学习

kiteq is a distributed mq framework

A distributed transactional large-scale NoSQL database powered by TiKV

A collection of TLA⁺ specifications of varying complexities

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

Verified Rust for low-level systems code

南京大学计算机系2020秋季形式语言与自动机实现

Source Code for 'Practical TLA+' by Hillel Wayne

JDK main-line development https://openjdk.org/projects/jdk

提升部署在cloudflare、vercel或netlify的网页在中国的访问速度和稳定性 Improve the access speed and stability in China of web pages hosted on cloudflare, vercel or netlify by merely changing your CNAME record. cf优选域名 | cf优…

Soot - A Java optimization framework

A LaTeX class for producing presentations and slides