я правильно улавливаю, что в тестах описывается референсная модель, потом в нее и в реальный инстанс идет флуд командами с сравнением итогового стейта, а потом это всё как-то сводится к минимальной последовательности команд для воспроизведения?

Мы делали модел-чекинг на SPIN/Promela. Пишешь модель на подмножестве Си (Promela), затем спинчекер елозит по state space и проверяет все углы. Выявило как минимум одну проблему.

Для неё есть ещё условия помимо детерменированности

Ну model checking не то же самое что property based тесты. В proper как правило подразумевается что модель уже без багов. Просто проверяется что реальная система ей соответствует

я правильно улавливаю, что в тестах описывается референсная модель, потом в нее и в реальный инстанс идет флуд командами с сравнением итогового стейта, а потом это всё как-то сводится к минимальной последовательности команд для воспроизведения?

если я правильно понимаю, то примерно так, но: ты не можешь повторно написать сложную систему, поэтому ты строишь массу простых срезов, проверяющих непротиворечивость и целостность данных

хочу поделиться впечатлением: у нас есть система, у неё есть некий стейт в базе данных и есть набор операций, которые этот стейт меняют (порядка 20 различных операций). В проде уже с год, более-менее работает.
Решили для неё сделать полный statefull property-based тест… выловили уже штук 8 багов / corner case / неконсистентностей. Часть из них требуют цепочек из 5-6 различных операций. В проде не проявлялось потому что пока что такая комбинация операций не использовалась в текущем продукте. Но очень довольны теперь что решили потратить на это время

У нас уже почти год проперные тесты как основные в сервисе и в целом очень удобно. Нашёл уже достаточно интересных багов. Особенно классные, которые связаны с фрагментированием пакетов в сети, и проявляются один раз на несколько тысяч. А так, времени своего точно стоят.

О, с фрагментированием баги отличные. Я уже как минимум два доморощенных фуззера написал для тех мест.

Да, я тоже раньше сам писал, потом на пропер переехал.

А не сталкивались с нечитаемыми ошибками от пропера? Или тем, что он падает с тем, что не может сгенерить тесткейс? Меня уже это немного подбешивать начинает. Поправил тест, он упал и чтобы понять почему, начинаешь пляски с бубнами и рассматривание кода на предмет ошибок.

Ему на вход нужен какой-то кусок данных, на которых что-то сломалось?
Или он сам вглядывается и генерирует хрень?

А не сталкивались с нечитаемыми ошибками от пропера? Или тем, что он падает с тем, что не может сгенерить тесткейс? Меня уже это немного подбешивать начинает. Поправил тест, он упал и чтобы понять почему, начинаешь пляски с бубнами и рассматривание кода на предмет ошибок.

Сгенерировать не может... ну у нас генератор умный и он от стейта генерирует команды возможные. И потом мы в precondition уже дополнительно перепроверяем.

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

Не нужно писать логику генерации. Просто говоришь, что у тебя, допустим на входе integer и binary и дальше он уже сам самые разные варианты перебирает.