# logicaffeine_verify > Z3-based static verification and model checking for Logicaffeine Every public module and item of `logicaffeine_verify`, module by module, each with its one-line summary and its address. Item pages hold the full signature, documentation, trait implementations and a link to the source. - Crate page: [logicaffeine_verify](https://docs.logicaffeine.com/logicaffeine_verify/) - All items on one page: [logicaffeine_verify/all](https://docs.logicaffeine.com/logicaffeine_verify/all) - Source: [src/logicaffeine_verify/lib.rs](https://docs.logicaffeine.com/src/logicaffeine_verify/lib.rs) - Every crate: [llms.txt](https://docs.logicaffeine.com/llms.txt) ## logicaffeine_verify - [mod abstraction](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/): Predicate Abstraction with CEGAR Refinement - [mod automata](https://docs.logicaffeine.com/logicaffeine_verify/automata/): Automata for Reactive Synthesis - [mod certificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/): Self-Certifying Proof Certificates - [mod compositional](https://docs.logicaffeine.com/logicaffeine_verify/compositional/): Assume-Guarantee Compositional Reasoning - [mod consistency](https://docs.logicaffeine.com/logicaffeine_verify/consistency/): Multi-Property Consistency Checking - [mod equivalence](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/): Semantic Equivalence Checking — The Core Contribution - [mod error](https://docs.logicaffeine.com/logicaffeine_verify/error/): Verification error types with Socratic error messages. - [mod ic3](https://docs.logicaffeine.com/logicaffeine_verify/ic3/): IC3/PDR (Property-Directed Reachability) - [mod incremental](https://docs.logicaffeine.com/logicaffeine_verify/incremental/): Incremental Verification - [mod interpolation](https://docs.logicaffeine.com/logicaffeine_verify/interpolation/): Interpolation-Based Model Checking - [mod ir](https://docs.logicaffeine.com/logicaffeine_verify/ir/): Verification IR (Intermediate Representation) - [mod kinduction](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/): k-Induction for Unbounded Safety Verification - [mod liveness](https://docs.logicaffeine.com/logicaffeine_verify/liveness/): Liveness-to-Safety Reduction - [mod multiclock](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/): Multi-Clock Domain Modeling - [mod parameterized](https://docs.logicaffeine.com/logicaffeine_verify/parameterized/): Parameterized Verification - [mod security](https://docs.logicaffeine.com/logicaffeine_verify/security/): Security Property Verification — Non-Interference - [mod smtlib](https://docs.logicaffeine.com/logicaffeine_verify/smtlib/): SMT-LIB2 Export - [mod solver](https://docs.logicaffeine.com/logicaffeine_verify/solver/): Z3 solver wrapper for Logicaffeine verification. - [mod strategy](https://docs.logicaffeine.com/logicaffeine_verify/strategy/): Strategy Selection Engine - [mod synthesis](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/): Reactive Synthesis from LTL - [mod type_infer](https://docs.logicaffeine.com/logicaffeine_verify/type_infer/): Constraint-based type inference for VerifyExpr. ## logicaffeine_verify::abstraction Predicate Abstraction with CEGAR Refinement - [struct AbstractModel](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/struct.AbstractModel) - [enum AbstractionResult](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/enum.AbstractionResult) - [fn abstract_model](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/fn.abstract_model): Create an abstract model from initial state and predicates (legacy 2-arg API). - [fn abstract_model_full](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/fn.abstract_model_full): Create an abstract model with Cartesian predicate abstraction. - [fn cegar_verify](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/fn.cegar_verify): CEGAR verification loop: abstract, check, refine. ## logicaffeine_verify::automata Automata for Reactive Synthesis - [struct AutomatonState](https://docs.logicaffeine.com/logicaffeine_verify/automata/struct.AutomatonState): A state in a Büchi automaton. - [struct AutomatonTransition](https://docs.logicaffeine.com/logicaffeine_verify/automata/struct.AutomatonTransition): A transition in a Büchi automaton. - [struct BuchiAutomaton](https://docs.logicaffeine.com/logicaffeine_verify/automata/struct.BuchiAutomaton): A Büchi automaton for LTL specifications. - [fn ltl_to_buchi](https://docs.logicaffeine.com/logicaffeine_verify/automata/fn.ltl_to_buchi): Convert an LTL specification to a Büchi automaton. ## logicaffeine_verify::certificate Self-Certifying Proof Certificates - [struct ProofCertificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/struct.ProofCertificate): A self-certifying proof certificate. - [struct ProofStep](https://docs.logicaffeine.com/logicaffeine_verify/certificate/struct.ProofStep): A single step in the proof. - [enum VerifyClaim](https://docs.logicaffeine.com/logicaffeine_verify/certificate/enum.VerifyClaim): What is being proven. - [fn digest_formula](https://docs.logicaffeine.com/logicaffeine_verify/certificate/fn.digest_formula): Compute a deterministic digest of a `VerifyExpr` for tamper detection. - [fn generate_equivalence_certificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/fn.generate_equivalence_certificate): Generate a proof certificate for an equivalence result. - [fn generate_safety_certificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/fn.generate_safety_certificate): Generate a proof certificate for a safety result. - [fn verify_certificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/fn.verify_certificate): Verify a proof certificate (check that steps are internally consistent). ## logicaffeine_verify::compositional Assume-Guarantee Compositional Reasoning - [struct ComponentSpec](https://docs.logicaffeine.com/logicaffeine_verify/compositional/struct.ComponentSpec): A component specification for compositional verification. - [enum CompositionalResult](https://docs.logicaffeine.com/logicaffeine_verify/compositional/enum.CompositionalResult): Result of compositional verification. - [fn verify_compositional](https://docs.logicaffeine.com/logicaffeine_verify/compositional/fn.verify_compositional): Verify a set of components compositionally. ## logicaffeine_verify::consistency Multi-Property Consistency Checking - [struct ConsistencyConfig](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.ConsistencyConfig): Configuration for spec consistency analysis. - [struct ConsistencyReport](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.ConsistencyReport): Full consistency analysis report. - [struct LabeledFormula](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.LabeledFormula): A formula labeled with its source text for error reporting. - [struct PairwiseConflict](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.PairwiseConflict): A pair of formulas that cannot hold simultaneously. - [struct RedundancyFinding](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.RedundancyFinding): A formula that is logically entailed by the remaining formulas. - [struct VacuityFinding](https://docs.logicaffeine.com/logicaffeine_verify/consistency/struct.VacuityFinding): A formula whose implication antecedent can never be satisfied. - [enum ConsistencyResult](https://docs.logicaffeine.com/logicaffeine_verify/consistency/enum.ConsistencyResult): Result of consistency checking (legacy API). - [enum SatisfiabilityResult](https://docs.logicaffeine.com/logicaffeine_verify/consistency/enum.SatisfiabilityResult): Whether the conjunction of all formulas is satisfiable. - [fn check_consistency](https://docs.logicaffeine.com/logicaffeine_verify/consistency/fn.check_consistency): Check if a set of properties can all hold simultaneously (legacy API). - [fn check_spec_consistency](https://docs.logicaffeine.com/logicaffeine_verify/consistency/fn.check_spec_consistency): Run full consistency analysis on a set of labeled formulas. ## logicaffeine_verify::equivalence Semantic Equivalence Checking — The Core Contribution - [struct CycleState](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/struct.CycleState): Signal assignments at a single clock cycle. - [struct EquivEncoder](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/struct.EquivEncoder): Encoder that handles Bool, Int, BitVec, and Array Z3 expressions for equivalence checking. - [struct Trace](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/struct.Trace): A counterexample trace showing signal values at each clock cycle. - [enum EquivalenceResult](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/enum.EquivalenceResult): Result of checking semantic equivalence. - [enum SignalValue](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/enum.SignalValue): Multi-sorted signal value for counterexample traces. - [fn check_equivalence](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/fn.check_equivalence): Check whether two VerifyExpr formulas are semantically equivalent. - [fn collect_int_vars_pub](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/fn.collect_int_vars_pub): Collect integer-typed variable names from a VerifyExpr (public API). - [fn collect_quantifier_bound_vars_pub](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/fn.collect_quantifier_bound_vars_pub): Collect quantifier-bound variables from a VerifyExpr (public API). - [fn collect_vars_pub](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/fn.collect_vars_pub): Collect all variable names referenced in a VerifyExpr (public API). - [fn extract_signals](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/fn.extract_signals): Extract unique signal names from a VerifyExpr by collecting Var references and stripping the @timestep suffix. ## logicaffeine_verify::error Verification error types with Socratic error messages. - [struct CounterExample](https://docs.logicaffeine.com/logicaffeine_verify/error/struct.CounterExample): A counterexample showing concrete values that falsify an assertion. - [struct VerificationError](https://docs.logicaffeine.com/logicaffeine_verify/error/struct.VerificationError): A verification error with Socratic explanation. - [enum VerificationErrorKind](https://docs.logicaffeine.com/logicaffeine_verify/error/enum.VerificationErrorKind): The category of verification error. - [type VerificationResult](https://docs.logicaffeine.com/logicaffeine_verify/error/type.VerificationResult): Result type for verification operations. ## logicaffeine_verify::ic3 IC3/PDR (Property-Directed Reachability) - [enum Ic3Result](https://docs.logicaffeine.com/logicaffeine_verify/ic3/enum.Ic3Result): Result of IC3/PDR verification. - [fn check_sat](https://docs.logicaffeine.com/logicaffeine_verify/ic3/fn.check_sat): Check if a formula is satisfiable (public, creates its own Z3 context). - [fn ic3](https://docs.logicaffeine.com/logicaffeine_verify/ic3/fn.ic3): Run IC3/PDR on a safety property. ## logicaffeine_verify::incremental Incremental Verification - [struct CachedResult](https://docs.logicaffeine.com/logicaffeine_verify/incremental/struct.CachedResult): Cached verification result. - [struct ChangeEvent](https://docs.logicaffeine.com/logicaffeine_verify/incremental/struct.ChangeEvent): A change event. - [struct VerificationCache](https://docs.logicaffeine.com/logicaffeine_verify/incremental/struct.VerificationCache): Verification cache. - [fn hash_property](https://docs.logicaffeine.com/logicaffeine_verify/incremental/fn.hash_property): Compute a hash for a property expression. - [fn verify_incremental](https://docs.logicaffeine.com/logicaffeine_verify/incremental/fn.verify_incremental): Verify properties incrementally. - [type PropertyHash](https://docs.logicaffeine.com/logicaffeine_verify/incremental/type.PropertyHash): A hash of a property for caching. ## logicaffeine_verify::interpolation Interpolation-Based Model Checking - [enum InterpolationResult](https://docs.logicaffeine.com/logicaffeine_verify/interpolation/enum.InterpolationResult): Result of interpolation-based model checking. - [fn interpolate](https://docs.logicaffeine.com/logicaffeine_verify/interpolation/fn.interpolate): Compute a Craig interpolant approximation. - [fn itp_model_check](https://docs.logicaffeine.com/logicaffeine_verify/interpolation/fn.itp_model_check): Interpolation-based model checking. ## logicaffeine_verify::ir Verification IR (Intermediate Representation) - [enum BitVecOp](https://docs.logicaffeine.com/logicaffeine_verify/ir/enum.BitVecOp): Bitvector operations for hardware verification. - [enum VerifyExpr](https://docs.logicaffeine.com/logicaffeine_verify/ir/enum.VerifyExpr): Expression AST for verification. - [enum VerifyOp](https://docs.logicaffeine.com/logicaffeine_verify/ir/enum.VerifyOp): Binary operations in the verification IR. - [enum VerifyType](https://docs.logicaffeine.com/logicaffeine_verify/ir/enum.VerifyType): Type declarations for verification variables. ## logicaffeine_verify::kinduction k-Induction for Unbounded Safety Verification - [struct SignalDecl](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/struct.SignalDecl): Signal declaration for k-induction. - [enum KInductionResult](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/enum.KInductionResult): Result of k-induction verification. - [fn encode_expr_bool](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/fn.encode_expr_bool): Simple recursive Bool encoder for k-induction formulas. - [fn encode_expr_int](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/fn.encode_expr_int): Try to encode an expression as a Z3 Int. Returns None if not integer-typed. - [fn instantiate_at](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/fn.instantiate_at): Instantiate an expression at a specific timestep by replacing @t with @{step}. - [fn instantiate_transition](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/fn.instantiate_transition): Instantiate a transition relation: replace @t with @{step} and @t’ with @{step+1}. - [fn k_induction](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/fn.k_induction): Run k-induction on a safety property. ## logicaffeine_verify::liveness Liveness-to-Safety Reduction - [enum LivenessResult](https://docs.logicaffeine.com/logicaffeine_verify/liveness/enum.LivenessResult): Result of liveness checking. - [fn check_liveness](https://docs.logicaffeine.com/logicaffeine_verify/liveness/fn.check_liveness): Check a liveness property via bounded search. ## logicaffeine_verify::multiclock Multi-Clock Domain Modeling - [struct ClockDomain](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/struct.ClockDomain) - [struct MultiClockModel](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/struct.MultiClockModel) - [enum MultiClockResult](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/enum.MultiClockResult) - [fn compute_schedule](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/fn.compute_schedule): Compute the interleaved firing schedule for a set of clock domains. - [fn verify_multiclock](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/fn.verify_multiclock): Verify a multi-clock domain design. ## logicaffeine_verify::parameterized Parameterized Verification - [enum ParameterizedResult](https://docs.logicaffeine.com/logicaffeine_verify/parameterized/enum.ParameterizedResult) - [fn verify_parameterized](https://docs.logicaffeine.com/logicaffeine_verify/parameterized/fn.verify_parameterized): Verify a parameterized property. ## logicaffeine_verify::security Security Property Verification — Non-Interference - [struct TaintedSignal](https://docs.logicaffeine.com/logicaffeine_verify/security/struct.TaintedSignal) - [enum SecurityLabel](https://docs.logicaffeine.com/logicaffeine_verify/security/enum.SecurityLabel) - [enum SecurityResult](https://docs.logicaffeine.com/logicaffeine_verify/security/enum.SecurityResult) - [fn check_non_interference](https://docs.logicaffeine.com/logicaffeine_verify/security/fn.check_non_interference): Check non-interference: public outputs independent of secret inputs. ## logicaffeine_verify::smtlib SMT-LIB2 Export - [fn equivalence_to_smtlib2](https://docs.logicaffeine.com/logicaffeine_verify/smtlib/fn.equivalence_to_smtlib2): Export an equivalence check to SMT-LIB2 format. - [fn to_smtlib2](https://docs.logicaffeine.com/logicaffeine_verify/smtlib/fn.to_smtlib2): Export a VerifyExpr to SMT-LIB2 format. ## logicaffeine_verify::solver Z3 solver wrapper for Logicaffeine verification. - [struct VerificationContext](https://docs.logicaffeine.com/logicaffeine_verify/solver/struct.VerificationContext): A verification context for building constraints incrementally. - [struct VerificationSession](https://docs.logicaffeine.com/logicaffeine_verify/solver/struct.VerificationSession): A verification session for working with the Verification IR. - [struct Verifier](https://docs.logicaffeine.com/logicaffeine_verify/solver/struct.Verifier): Low-level Z3-based verifier for single-shot validity checks. - [fn rename_var_in_expr](https://docs.logicaffeine.com/logicaffeine_verify/solver/fn.rename_var_in_expr): Rename a variable in a VerifyExpr (simple textual substitution). Recursively traverses ALL variants — no silent drops. ## logicaffeine_verify::strategy Strategy Selection Engine - [enum Strategy](https://docs.logicaffeine.com/logicaffeine_verify/strategy/enum.Strategy): Verification strategy. - [enum VerificationResult](https://docs.logicaffeine.com/logicaffeine_verify/strategy/enum.VerificationResult): Unified verification result from auto-selection. - [fn select_strategy](https://docs.logicaffeine.com/logicaffeine_verify/strategy/fn.select_strategy): Select the best strategy based on property structure. - [fn verify_auto](https://docs.logicaffeine.com/logicaffeine_verify/strategy/fn.verify_auto): Verify a property using automatic strategy selection. ## logicaffeine_verify::synthesis Reactive Synthesis from LTL - [struct Circuit](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/struct.Circuit): A synthesized controller circuit. - [struct CircuitTransition](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/struct.CircuitTransition): A single transition in the synthesized circuit. - [struct SignalDecl](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/struct.SignalDecl): Signal declaration for synthesis. - [enum SynthesisResult](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/enum.SynthesisResult): Result of reactive synthesis. - [fn circuit_to_sva](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/fn.circuit_to_sva): Generate SVA monitor from a synthesized circuit. - [fn circuit_to_verilog](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/fn.circuit_to_verilog): Generate Verilog RTL from a synthesized circuit. - [fn synthesize_from_ltl](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/fn.synthesize_from_ltl): Synthesize a controller from an LTL specification. ## logicaffeine_verify::type_infer Constraint-based type inference for VerifyExpr. - [enum TypeError](https://docs.logicaffeine.com/logicaffeine_verify/type_infer/enum.TypeError) - [fn infer_types](https://docs.logicaffeine.com/logicaffeine_verify/type_infer/fn.infer_types): Infer types for all variables in a VerifyExpr.