Die korrekte Funktion der Methode und die Voraussetzung das sie ihren Contract einhält würdest Du mit
Unit-Tests abdecken.
Daher ist die Prüfung des 'Innenverhältnisses' des Vertrages nicht so relevant. Das 'Aussenverhältnis' ist das, was für eine solche Codeanalyse wirklich relevant ist.
Wenn die Nachbedingung nicht passt weil Dein Random.NextInt(max) sich falsch verhält und Werte > max liefert, dann wird das klar erst zur Laufzeit auffallen. Aber in aller Regel wird sowas eben entsprechend gut getestet sein damit das nicht passiert.