Для скриптов на Питоне появилась экспериментальная библиотека | Протестировал

Для скриптов на Питоне появилась экспериментальная библиотека CrossHair, которая без выполнения программы ищет возможные пути выполнения и контрпримеры с помощью SMT-решателя (сейчас это популярный Z3). Для указания желаемого поведения программы можно использовать три способа: стандартные ассерты, PEP 316 и с помощью декораторов icontract. Авторы подчеркивают экспериментальный статус модуля: "Be aware that the absence of a counterexample does not guarantee that the property holds.". До появления CrossHair уже были похожие реализации (PEF: Python Error Finder, PyExZ3), но CrossHair является более полной реализацией идеи за счет поддержки символьных списков, словарей и коллекций. Есть интеграция с популярными IDE. Если интересны детали реализации, то они есть в документации и в публикации.

Зачем вообще это нужно? Разные инструменты находят разные баги. Если есть возможность раньше ("shift-left") и дешевле находить проблемы в коде, то почему бы этого не делать? В документации авторы ещё и проиллюстрировали аргументы.