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 thos

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. [0] https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html