https://www.microsoft.com/en-us/research/blog/p-programming-... makes the case better than I can on why it's important to have the specification and implementation come from the same source as opposed to maintaining two and then verify via traces that they're compatible.

But definitely worth doing (like Jepsen does) to find problems in the implementation.