そんなときこそFormal methods
複雑になるとUndecidableなのが玉に瑕