Hillel is a software engineer specializing in formal methods, distributed systems, and software history. He is the author of Practical TLA+ and the Crossover Project. He has done formal verification and training for clients like NASA, Meta, Giesecke+Devrient, McKinsey, Siemens, and Western Digital. In his free time, he juggles and makes chocolate. He has a blog at hillelwayne.com and a newsletter at https://buttondown.email/hillelwayne/.