Does the linked case study[0] help at all? It's real code that already had debug assertions that acted as a postcondition. It was than formally proved that those conditions held (or didn't hold in one case) for all the relevant functions.
It does help. what I find interesting here is that the prover was able to find a potential bug that the test cases were not able to find. That's powerful.