> The tool the researchers designed for this proof is called IC3PO, a model checking system that looks through every state a program can enter and determines wh

> The tool the researchers designed for this proof is called IC3PO, a model checking system that looks through every state a program can enter and determines whether it matches a description of safe behavior. If the protocol is correct, IC3PO produces what’s termed an inductive invariant—a proof by induction that the property holds in all cases. If instead a bug is found in the protocol, it will produce a counter-example and execution trace, showing step by step how the bug manifests. That's really cool.