Comment by uvdn7

The "hard problem" defined here is more about the engineering side. The analogy I have is Paxos the protocol and Google's Paxos Made Live paper. We do have many cache coherency protocols that are provably correct (using TLA+ if you will); but making them actually consistent in production is a completely different story; and a hard problem for an invalidation-based cache.