Congrats Hillel, great work. A teammate used TLA+ at work to help diagnosis a deadlock bug due to a lock issue in postgres, and since then I've been mesmerized

Congrats Hillel, great work. A teammate used TLA+ at work to help diagnosis a deadlock bug due to a lock issue in postgres, and since then I've been mesmerized by its simplicity and power to prove simple invariants over complex specs. Looking forward to reading more!