The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thi

The way I think of it is that TLA+ is a tool for ensuring that the thing you intended to write will work. It's not a tool for checking whether you wrote the thing you intended to.