The CZT verification condition generator supports generating conjectures about Z specifications used to verify their correctness and consistency.

The following verification conditions are supported:

• Domain checks (function application, axiomatic definitions, etc.)
• Feasibility checks (operation preconditions)
• Refinement checks (refinement correctness, experimental)