В книге "Verification of sequential and concurrent programs" есть раздел 1.5 Assertional Methods in Practice где написано:
> -- Цитата:
> Checking whether an implementation (a program) satisfies a contract isdone  (as outlined above)  —ina limited way— . The second approach requires that the assertionsin the contracts are Boolean expressions. Then during each particular run ofthe implementation it is checked automatically whether along this run allassertions of the contract are satisfied. If an assertion is encountered that isnot satisfied, a failure or exception is raised.
Перевод:
> -- Цитата:
> Проверка того, удовлетворяет ли реализация (программы) контракту, проводится , используя правила доказательств (как описано выше) . Второй подход требует чтобы утверждения контрактов были логическими выражениями. Затем во время каждого запуска программы все утверждения вдоль пути выполнения автоматически проверяются на то, что они выполняются. Если обнаруживается, что утверждение не выполняется, то возникает ошибка или исключение.

Таким образом, можно вообще не использовать assert в runtime, а использовать первый подход: формальная верификация.