[pfdietz]

If you can specify your program (or a part of it) well enough to prove it correct, you can also use that specification for property-based testing.