Сергей Соловьев

Если хочешь упороться, то можно заюзать формальные верификаторы.
Например, SPIN.

Он использует свой язык, поэтому придется дублировать логику.
На так можно удостовериться в корректности.