TLA+ is a tool to design system and algorithms, then programmatically verify that those systems do not have critical bugs. Engineers at Amazon use TLA+ to prevent serious but subtle bugs from reaching production. They have used TLA+ on 10 large complex real-world systems.