.

Как??

Нам надо автоматически вывести нужные стратегии и проперти для условного hypothesis из кода, а затем построить формальное доказательство, а не просто нагенерить тучи случайных тестов.
Автоматизировать труд самых дорогих и редких экспертов в этой темке!
То есть надо автоматически выводить подобные инварианты и контракты из семантики кода, или даже из простой спецификации, + даже обходиться без перебора, применяя символьное "выполнение".

Системы вроде Astree, Coverity, CodeQL, Frama-C -- это по сути просто продвинутые линтеры. Ну, да, Astree умеет даже формально доказывать отсутствие определённых классов ошибок в критическом софте (авиационная/автомобильная промышленность), но весьма ограниченно.

А продвинутое решение должно само выдвигать гипотезы о свойствах кода, и доказывать математически, что ошибок нет для всего пространства входных данных. В крайнем случае -- точное описание всех условий, при которых код работает, которые мы затем можем задать непосредственно на статической системе типов, чтобы компилятор это контролировал.

(тут мы сваливаемся в Гёделя, проблему полноты, и философские вопросы :)

Даже если применять для этой цели в лоб пруверы вроде Lean4, человеку всё равно придётся строить пошаговое доказательство из мелких лемм, а так как каждая лямбда требует копипасты контекста, мы получаем экспоненциальный рост от размера доказательства. Так собственно сегодня и делается, и эти проекты стоят многие миллионы долларов.

Так вот какая идея: создаём вычислительную процедуру, которая за один проход преобразует программу как исходный терм в конечный. Корректность доказывается один раз!

В лине например есть Parametric Higher-Order Abstract Syntax, и если мы делегируем связывания его системе типов, то избегаем явной муторщины с de bruijn индексами, и получаем близкую к линейной производительность!
Subterm sharing явно поддерживается на уровне структур данных, и в итоге и rewriting и бета-редукция выполняются за один проход в рамках единой рефлексивной процедуры!! А side conditions при этом проверяем автоматически во время паттерн-матчинга!!!

Выигрыш по времени и по цене? Ну, где-то единицы...десятки тысяч раз. Для Fiat Cryptography например был выигрыш в тысячу, но в чисто академическом эксперименте, и математика там применялась не очень продвинутая.

Резюме: Hypothesis даёт статистическую уверенность, просто некоторую вероятность, механически перебирая мириады случаев. Идея, о которой я рассказал, автоматически доказывает корректность всей процедуры rewriting, приближается к формальной гарантии для всех входных данных. Она не просто найдёт баг в approx_max_k, а сгенерирует доказательство его математической эквивалентности k-топу антропика (или найдёт все условия, когда это не так).