I did an analysis of the bug from the blog post and the TAO paper, and from what I can tell the fundamental bug is therefore the fact that the error handler that handles cache invalidation errors drops only lesser versions, while the cache invalidation contract requires replacing equal or lesser versions.
Formal modeling is a mathematical approach for designing and checking correctness of software systems. It focuses on standard software engineering and distributed systems problems of the sort programmers face every day. It takes a pragmatic engineering approach: each problem starts with UML diagrams, design decisions and sometimes even a requirements document. We work through how to get from a whiteboard design to an initial mathematical model. Then we refine it based on logical errors found by the model checker, which return with a level of detail unheard of in a standard debugger. Formal modeling is a skill every engineer should have in their toolbox.
All the examples are downloadable, and their is a quick setup section at the start. Additionally, there is an explorable model error debugger build right into the website.
There is a detailed write up here: https://elliotswart.github.io/pragmaticformalmodeling/cachin...