> is certainly not sufficient to assume correctness of an implementation

Indeed. This is where tools like Jepsen and good fuzz testing can help.