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.

Can you speak more on why ‘making them actually consistent in production is a completely different story’?

Curious because I’ve been learning TLA+ recently and interested to more know about cases where an algorithm has been proven but actual an implementation of it fails.

Let try to put this as concisely as possible. When you put an algorithm in code, when rubber hits the road, you have to make certain assumptions of how things work, eg how events are ordered, how fsync works, what kind of failure scenarios you are expecting, etc. More likely than not, the reality will be a little different. No to measure just innocent bugs in the code.

My favorite example is Paxos. Its algorithm fits on a single slide. But it’s notoriously hard to make it actually work correctly in production.