That's too bad, those guys were hilarious. Here's Leslie Lamport solving one of the Car Talk puzzles with TLA+:
https://github.com/fintler/tlaplus/raw/master/examples/CarTa...
https://github.com/fintler/tlaplus/raw/master/examples/CarTa...
Regardless, oh my goodness. When you see the solution spit out you just wanna drop your head on the desk. It's that "ahaaa" moment we probably don't feel often enough.