Production Verification Engine

This release transforms the verification modules from proof-of-concept implementations into production-grade engines with full algorithmic depth.

IC3/PDR Model Checking

Complete IC3 implementation with frame management, counterexample-guided generalization, and inductive invariant extraction. Proves unbounded safety properties without requiring a bound parameter.

K-Induction & Interpolation

K-induction with auxiliary invariant strengthening for properties that require inductive proofs. Craig interpolation extracts predicates from refutation proofs for automatic abstraction refinement.

CEGAR Abstraction Refinement

Full CEGAR loop: predicate abstraction builds an abstract model, model checking finds abstract counterexamples, feasibility checking detects spurious traces, and interpolation discovers new predicates to refine the abstraction.

Liveness & Multi-Clock

Liveness checking with fairness constraints and ranking functions, including liveness-to-safety reduction for tool interoperability. Multi-clock verification handles synchronizer correctness, metastability windows, and clock domain interaction proofs.

Compositional Verification

Assume-guarantee reasoning with contract decomposition, circular compositional proofs, and interface refinement checking. Enables verification of large designs by decomposing into independently verifiable components.

Synthesis & Security

Expanded reactive synthesis oracle with realizability checking. Security property verification with information flow analysis and non-interference checking for hardware designs.