静的解析
システムコードはいくつかのコード品質チェックを通過します。
一貫性チェック
仕様は一貫性がチェックされます。仕様が充足不可能かもしれない場合、警告が生成されます：
signal x: Float
spec main = always (x > 0 && x < 0)
これは、どのシステムもこの仕様を満たすことができないため、仕様に問題があることを意味します。
仕様間の不整合もユーザーに報告されます：
signal x: Float
spec always_positive = always (x > 0)
spec always_negative = always (x < 0)
この場合、各仕様は単独では充足可能ですが、いかなるシステムもこれら両方ともを満たすことはできません。
冗長性チェック
ある仕様が、システムの他の仕様によって暗黙的に示されているために冗長である場合、これも検出されます：
signal x: Float
spec positive_becomes_negative = always (x > 0 => eventually x < 0)
spec sometimes_positive = eventually x > 0
spec sometimes_negative = eventually x < 0
この場合、sometimes_negativeという仕様が冗長であることをユーザーに警告します。なぜなら、このプロパティはpositive_becomes_negativeとsometimes_positiveの組み合わせによって既に暗示されているためです。実際、sometimes_positiveはx > 0となる時点が存在することを意味し、positive_becomes_negativeに基づけば、その時点以後に x < 0となる時点が存在しなければならないと結論付けられます。