I routinely write a simple implementation with tests, then a fast implementation that passes the same tests, then check the two did the same thing on every call

I routinely write a simple implementation with tests, then a fast implementation that passes the same tests, then check the two did the same thing on every call in a debug/contracts build. Mix it with design by contact as the sibling post suggests and you get 'postcondition: did same thing as the simple implementation', which combined with tests to check said thing was broadly sensible, seems to suffice.