TLA+ Practice Currently contains: An attempt to model the MayhemMandril system from Lynn Root's Async Python Tutorial (WIP)