There are "lightweight formal methods". Most problems can be produced via small models. Tools like alloy are built around this idea. (IIRC alloy was used to sho

There are "lightweight formal methods". Most problems can be produced via small models. Tools like alloy are built around this idea. (IIRC alloy was used to show that a famous DHT had issues with the churn protocol) https://en.wikipedia.org/wiki/Alloy_(specification_language) https://en.wikipedia.org/wiki/Alloy_(specification_language)