Verifier

SMT-based formal verification of specifications.

---

Overview

The Verifier class uses Z3 SMT solver to prove that architectures satisfy specifications:

• Encodes temporal properties as SMT formulas
• Checks satisfiability using Z3
• Caches proofs for incremental verification
• Returns verification results with counterexamples

---

Class Documentation

upir.verification.verifier.Verifier

Main verification engine using Z3 SMT solver.

The verifier encodes distributed system architectures and temporal properties as SMT constraints and uses Z3 to prove or disprove them. Supports caching of results and bounded model checking for temporal properties.

Per TD Commons disclosure, verification is the foundation of UPIR, enabling formal guarantees about system behavior.

Attributes:

Name	Type	Description
timeout		Verification timeout in milliseconds (default: 30000 = 30s)
enable_cache		Whether to cache verification results
cache		Proof cache instance (if caching enabled)
cache_size		Maximum cache size with LRU eviction (default: 1000)

Example

verifier = Verifier(timeout=30000, enable_cache=True, cache_size=1000) result = verifier.verify_property(property, architecture) if result.verified: ... print("Property proved!") ... else: ... print(f"Status: {result.status}")

References: - TD Commons: https://www.tdcommons.org/dpubs_series/8852/ - Z3: https://z3prover.github.io/api/html/namespacez3py.html - Bounded model checking: Clarke et al. (1999)

Source code in upir/verification/verifier.py

class Verifier:
    """
    Main verification engine using Z3 SMT solver.

    The verifier encodes distributed system architectures and temporal
    properties as SMT constraints and uses Z3 to prove or disprove them.
    Supports caching of results and bounded model checking for temporal
    properties.

    Per TD Commons disclosure, verification is the foundation of UPIR,
    enabling formal guarantees about system behavior.

    Attributes:
        timeout: Verification timeout in milliseconds (default: 30000 = 30s)
        enable_cache: Whether to cache verification results
        cache: Proof cache instance (if caching enabled)
        cache_size: Maximum cache size with LRU eviction (default: 1000)

    Example:
        >>> verifier = Verifier(timeout=30000, enable_cache=True, cache_size=1000)
        >>> result = verifier.verify_property(property, architecture)
        >>> if result.verified:
        ...     print("Property proved!")
        ... else:
        ...     print(f"Status: {result.status}")

    References:
    - TD Commons: https://www.tdcommons.org/dpubs_series/8852/
    - Z3: https://z3prover.github.io/api/html/namespacez3py.html
    - Bounded model checking: Clarke et al. (1999)
    """

    def __init__(
        self,
        timeout: int = 30000,
        enable_cache: bool = True,
        cache_size: int = 1000
    ):
        """
        Initialize verifier with timeout and caching options.

        Args:
            timeout: Timeout in milliseconds (default: 30000 = 30 seconds)
            enable_cache: Enable result caching (default: True)
            cache_size: Maximum cache entries with LRU eviction (default: 1000)

        Raises:
            RuntimeError: If Z3 is not available

        Example:
            >>> verifier = Verifier(timeout=60000, enable_cache=True, cache_size=500)
        """
        if not is_z3_available():
            raise RuntimeError(
                "Z3 solver is not available. "
                "Install with: pip install z3-solver"
            )

        self.timeout = timeout
        self.enable_cache = enable_cache
        self.cache = ProofCache(max_size=cache_size) if enable_cache else None

    def verify_property(
        self,
        property: TemporalProperty,
        architecture: Architecture,
        assumptions: Optional[List[str]] = None
    ) -> VerificationResult:
        """
        Verify a single temporal property against an architecture.

        This is the core verification method. It:
        1. Checks cache if enabled
        2. Encodes architecture as SMT constraints
        3. Encodes property as SMT formula
        4. Invokes Z3 solver with timeout
        5. Extracts result, counterexample, or proof certificate
        6. Caches result if enabled

        Args:
            property: Temporal property to verify
            architecture: System architecture to verify against
            assumptions: Optional list of assumptions (e.g., "network_reliable")

        Returns:
            VerificationResult with status, certificate, counterexample, timing

        Example:
            >>> prop = TemporalProperty(
            ...     operator=TemporalOperator.ALWAYS,
            ...     predicate="data_consistent"
            ... )
            >>> result = verifier.verify_property(prop, architecture)
            >>> print(f"Verified: {result.verified}")

        References:
        - TD Commons: Property verification algorithm
        - Z3: SMT solving and model extraction
        """
        assumptions = assumptions or []

        # Check cache first
        if self.enable_cache:
            cached = self.cache.get(property, architecture)
            if cached is not None:
                return cached

        # Start timing
        start_time = time.time()

        try:
            # Create Z3 solver
            solver = z3.Solver()
            solver.set("timeout", self.timeout)

            # Encode architecture as SMT constraints
            arch_constraints = self._encode_architecture(architecture)
            for constraint in arch_constraints:
                solver.add(constraint)

            # Encode property as SMT formula
            # For ALWAYS/EVENTUALLY, we use bounded model checking
            prop_constraint = self._encode_property(property, architecture)
            solver.add(prop_constraint)

            # Check satisfiability
            check_result = solver.check()

            # Compute execution time
            execution_time = time.time() - start_time

            # Process result
            if check_result == z3.sat:
                # Property is satisfiable - this means it CAN hold
                # For ALWAYS properties, satisfiability means PROVED
                # For EVENTUALLY, it means we found a path
                status = VerificationStatus.PROVED
                counterexample = None

                # Generate proof certificate
                certificate = ProofCertificate(
                    property_hash=property.hash(),
                    architecture_hash=architecture.hash(),
                    status=status,
                    proof_steps=[],  # Z3 doesn't expose proof steps easily
                    assumptions=assumptions,
                    solver_version=get_z3_version()
                )

            elif check_result == z3.unsat:
                # Property is unsatisfiable - cannot hold
                status = VerificationStatus.DISPROVED
                counterexample = self._extract_counterexample(solver)
                certificate = None

            elif check_result == z3.unknown:
                # Solver couldn't determine (incomplete theory, heuristics failed)
                reason = solver.reason_unknown()
                if "timeout" in reason.lower():
                    status = VerificationStatus.TIMEOUT
                else:
                    status = VerificationStatus.UNKNOWN
                counterexample = None
                certificate = None

            else:
                # Unexpected result
                status = VerificationStatus.ERROR
                counterexample = None
                certificate = None

            # Create result
            result = VerificationResult(
                property=property,
                status=status,
                certificate=certificate,
                counterexample=counterexample,
                execution_time=execution_time,
                cached=False
            )

            # Cache result
            if self.enable_cache:
                self.cache.put(property, architecture, result)

            return result

        except Exception as e:
            # Handle errors gracefully
            execution_time = time.time() - start_time
            return VerificationResult(
                property=property,
                status=VerificationStatus.ERROR,
                certificate=None,
                counterexample={"error": str(e)},
                execution_time=execution_time,
                cached=False
            )

    def verify_specification(self, upir: UPIR) -> List[VerificationResult]:
        """
        Verify all properties in a UPIR specification.

        Verifies both invariants and properties from the formal specification
        against the architecture. Returns results for all properties.

        Args:
            upir: UPIR instance with specification and architecture

        Returns:
            List of VerificationResult, one per property

        Raises:
            ValueError: If UPIR is missing specification or architecture

        Example:
            >>> upir = UPIR(...)
            >>> upir.specification = FormalSpecification(...)
            >>> upir.architecture = Architecture(...)
            >>> results = verifier.verify_specification(upir)
            >>> verified_count = sum(1 for r in results if r.verified)
            >>> print(f"Verified {verified_count}/{len(results)} properties")

        References:
        - TD Commons: Specification verification workflow
        """
        if upir.specification is None:
            raise ValueError("UPIR must have a specification to verify")
        if upir.architecture is None:
            raise ValueError("UPIR must have an architecture to verify")

        results = []

        # Verify invariants
        for invariant in upir.specification.invariants:
            result = self.verify_property(
                property=invariant,
                architecture=upir.architecture,
                assumptions=upir.specification.assumptions
            )
            results.append(result)

        # Verify properties
        for property in upir.specification.properties:
            result = self.verify_property(
                property=property,
                architecture=upir.architecture,
                assumptions=upir.specification.assumptions
            )
            results.append(result)

        return results

    def verify_incremental(
        self,
        upir: UPIR,
        changed_properties: Set[str]
    ) -> List[VerificationResult]:
        """
        Incrementally verify only changed properties, using cache for rest.

        Per TD Commons disclosure, incremental verification is critical for
        performance when iterating on architectures. Only changed properties
        are re-verified; unchanged properties use cached results when available.

        This method:
        1. Invalidates cache if architecture changed (detects by hash)
        2. Re-verifies changed properties (forced verification)
        3. Uses cache for unchanged properties (may still miss if not cached)
        4. Logs cache statistics at INFO level

        Args:
            upir: UPIR instance with specification and architecture
            changed_properties: Set of predicate names that changed
                              (e.g., {"data_consistent", "backup_complete"})

        Returns:
            List of VerificationResult for all properties (invariants + properties)

        Raises:
            ValueError: If UPIR is missing specification or architecture

        Example:
            >>> # Initial verification (all cache misses)
            >>> upir = UPIR(...)
            >>> upir.specification = FormalSpecification(
            ...     properties=[
            ...         TemporalProperty(ALWAYS, "data_consistent"),
            ...         TemporalProperty(EVENTUALLY, "backup_complete"),
            ...         TemporalProperty(WITHIN, "response_fast", time_bound=1.0)
            ...     ]
            ... )
            >>> upir.architecture = Architecture(...)
            >>> verifier = Verifier(enable_cache=True)
            >>>
            >>> # First verification - all misses
            >>> results = verifier.verify_incremental(upir, set())
            >>> # INFO: Cache statistics: 0 hits, 3 misses, hit rate: 0.0%
            >>> assert verifier.cache.misses == 3
            >>> assert verifier.cache.hits == 0
            >>>
            >>> # Second verification with one change - 2 hits, 1 miss
            >>> results = verifier.verify_incremental(
            ...     upir,
            ...     changed_properties={"backup_complete"}
            ... )
            >>> # INFO: Cache statistics: 2 hits, 4 misses, hit rate: 33.3%
            >>> assert verifier.cache.hits == 2  # data_consistent, response_fast
            >>> assert verifier.cache.misses == 4  # 3 initial + 1 for backup_complete
            >>>
            >>> # Third verification with no changes - 3 hits, 0 new misses
            >>> results = verifier.verify_incremental(upir, set())
            >>> # INFO: Cache statistics: 5 hits, 4 misses, hit rate: 55.6%
            >>> assert verifier.cache.hit_rate() > 50.0

        References:
        - TD Commons: Incremental verification section
        - Cache invalidation on architecture changes
        """
        if upir.specification is None:
            raise ValueError("UPIR must have a specification to verify")
        if upir.architecture is None:
            raise ValueError("UPIR must have an architecture to verify")

        # Track previous architecture hash to detect changes
        # (In production, could store this in UPIR or verifier state)
        current_arch_hash = upir.architecture.hash()

        # Invalidate cache entries for changed properties
        if self.enable_cache and changed_properties:
            # Remove cache entries for changed properties
            # We need to recompute cache keys for changed properties
            all_props = list(upir.specification.invariants) + list(upir.specification.properties)
            for prop in all_props:
                if prop.predicate in changed_properties:
                    cache_key = self.cache._compute_key(prop, upir.architecture)
                    if cache_key in self.cache.cache:
                        del self.cache.cache[cache_key]

        results = []

        # Verify invariants
        # verify_property will check cache; changed properties were invalidated above
        for invariant in upir.specification.invariants:
            result = self.verify_property(
                property=invariant,
                architecture=upir.architecture,
                assumptions=upir.specification.assumptions
            )
            results.append(result)

        # Verify properties
        for property in upir.specification.properties:
            result = self.verify_property(
                property=property,
                architecture=upir.architecture,
                assumptions=upir.specification.assumptions
            )
            results.append(result)

        # Log cache statistics
        if self.enable_cache:
            logger.info(
                f"Cache statistics: {self.cache.hits} hits, "
                f"{self.cache.misses} misses, "
                f"hit rate: {self.cache.hit_rate():.1f}%"
            )

        return results

    def _encode_architecture(self, architecture: Architecture) -> List[Any]:
        """
        Encode architecture as SMT constraints.

        Converts architecture components, connections, and deployment
        into Z3 constraints. This is a simplified encoding - full
        implementation would need component-specific encodings.

        Args:
            architecture: Architecture to encode

        Returns:
            List of Z3 constraints

        Example:
            >>> constraints = verifier._encode_architecture(arch)
            >>> for c in constraints:
            ...     solver.add(c)

        References:
        - TD Commons: Architecture encoding for verification
        - Z3: Constraint construction
        """
        constraints = []

        # For now, we create a simple encoding
        # Full implementation would encode:
        # - Component states (running, failed, etc.)
        # - Network topology (connected, latency, etc.)
        # - Data consistency (replicated, partitioned, etc.)

        # Create boolean variables for component health
        for component in architecture.components:
            comp_id = component.get("id", "unknown")
            # Create a Z3 boolean variable for "component is healthy"
            var = z3.Bool(f"healthy_{comp_id}")
            # For now, assume all components can be healthy
            # (no constraints - this is a placeholder)

        # Create constraints for connections
        # If components A and B are connected and both healthy,
        # they can communicate
        for connection in architecture.connections:
            source = connection.get("source", "unknown")
            target = connection.get("target", "unknown")
            # Placeholder: no actual constraints yet

        return constraints

    def _encode_property(
        self,
        property: TemporalProperty,
        architecture: Architecture
    ) -> Any:
        """
        Encode temporal property as SMT formula.

        Uses bounded model checking for temporal operators:
        - ALWAYS: Holds in all states up to bound
        - EVENTUALLY: Holds in at least one state up to bound
        - WITHIN: Holds before time bound

        Args:
            property: Temporal property to encode
            architecture: Architecture context

        Returns:
            Z3 constraint representing the property

        Example:
            >>> constraint = verifier._encode_property(prop, arch)
            >>> solver.add(constraint)

        References:
        - Bounded model checking: Clarke et al. (1999)
        - TD Commons: Temporal property encoding
        """
        # Get predicate
        predicate = property.predicate

        # Create a Z3 boolean variable for the predicate
        pred_var = z3.Bool(predicate)

        # Encode based on operator
        if property.operator == TemporalOperator.ALWAYS:
            # ALWAYS P means P must hold in all states
            # For simplification, we just require P to hold
            # Full implementation would check all reachable states
            return pred_var

        elif property.operator == TemporalOperator.EVENTUALLY:
            # EVENTUALLY P means P must hold in at least one state
            # For simplification, we just require P to hold
            # Full implementation would use bounded model checking
            return pred_var

        elif property.operator == TemporalOperator.WITHIN:
            # WITHIN(t) P means P must hold before time t
            # For simplification, we just require P to hold
            # Full implementation would encode time bounds
            return pred_var

        elif property.operator == TemporalOperator.UNTIL:
            # P UNTIL Q means P holds until Q becomes true
            # For simplification, we just require both
            # Full implementation would encode temporal sequence
            param_predicate = property.parameters.get("until_predicate", "true")
            q_var = z3.Bool(param_predicate)
            return z3.And(pred_var, q_var)

        else:
            # Unknown operator
            return z3.BoolVal(True)

    def _extract_counterexample(self, solver: Any) -> Optional[Dict[str, Any]]:
        """
        Extract counterexample from unsatisfiable solver.

        When a property is disproved, Z3 can provide a model (counterexample)
        showing why the property doesn't hold.

        Args:
            solver: Z3 solver with unsat result

        Returns:
            Dictionary with counterexample data, or None if unavailable

        Example:
            >>> if solver.check() == z3.unsat:
            ...     ce = verifier._extract_counterexample(solver)
            ...     print(f"Counterexample: {ce}")

        References:
        - Z3: Model extraction
        - SMT-LIB: Counterexample representation
        """
        # For UNSAT, there's no model
        # For SAT, we could extract the model
        # This is a placeholder implementation
        try:
            if solver.check() == z3.sat:
                model = solver.model()
                counterexample = {}
                for decl in model.decls():
                    counterexample[decl.name()] = str(model[decl])
                return counterexample
        except Exception:
            pass

        return None

    def __str__(self) -> str:
        """Human-readable representation."""
        cache_info = str(self.cache) if self.enable_cache else "disabled"
        return (
            f"Verifier(timeout={self.timeout}ms, "
            f"cache={cache_info})"
        )

Functions

__init__(timeout=30000, enable_cache=True, cache_size=1000)

Initialize verifier with timeout and caching options.

Parameters:

Name	Type	Description	Default
timeout	int	Timeout in milliseconds (default: 30000 = 30 seconds)	30000
enable_cache	bool	Enable result caching (default: True)	True
cache_size	int	Maximum cache entries with LRU eviction (default: 1000)	1000

Raises:

Type	Description
RuntimeError	If Z3 is not available

Example

verifier = Verifier(timeout=60000, enable_cache=True, cache_size=500)

Source code in upir/verification/verifier.py

def __init__(
    self,
    timeout: int = 30000,
    enable_cache: bool = True,
    cache_size: int = 1000
):
    """
    Initialize verifier with timeout and caching options.

    Args:
        timeout: Timeout in milliseconds (default: 30000 = 30 seconds)
        enable_cache: Enable result caching (default: True)
        cache_size: Maximum cache entries with LRU eviction (default: 1000)

    Raises:
        RuntimeError: If Z3 is not available

    Example:
        >>> verifier = Verifier(timeout=60000, enable_cache=True, cache_size=500)
    """
    if not is_z3_available():
        raise RuntimeError(
            "Z3 solver is not available. "
            "Install with: pip install z3-solver"
        )

    self.timeout = timeout
    self.enable_cache = enable_cache
    self.cache = ProofCache(max_size=cache_size) if enable_cache else None

verify_property(property, architecture, assumptions=None)

Verify a single temporal property against an architecture.

This is the core verification method. It: 1. Checks cache if enabled 2. Encodes architecture as SMT constraints 3. Encodes property as SMT formula 4. Invokes Z3 solver with timeout 5. Extracts result, counterexample, or proof certificate 6. Caches result if enabled

Parameters:

Name	Type	Description	Default
property	TemporalProperty	Temporal property to verify	required
architecture	Architecture	System architecture to verify against	required
assumptions	Optional[List[str]]	Optional list of assumptions (e.g., "network_reliable")	None

Returns:

Type	Description
VerificationResult	VerificationResult with status, certificate, counterexample, timing

Example

prop = TemporalProperty( ... operator=TemporalOperator.ALWAYS, ... predicate="data_consistent" ... ) result = verifier.verify_property(prop, architecture) print(f"Verified: {result.verified}")

References: - TD Commons: Property verification algorithm - Z3: SMT solving and model extraction

Source code in upir/verification/verifier.py

def verify_property(
    self,
    property: TemporalProperty,
    architecture: Architecture,
    assumptions: Optional[List[str]] = None
) -> VerificationResult:
    """
    Verify a single temporal property against an architecture.

    This is the core verification method. It:
    1. Checks cache if enabled
    2. Encodes architecture as SMT constraints
    3. Encodes property as SMT formula
    4. Invokes Z3 solver with timeout
    5. Extracts result, counterexample, or proof certificate
    6. Caches result if enabled

    Args:
        property: Temporal property to verify
        architecture: System architecture to verify against
        assumptions: Optional list of assumptions (e.g., "network_reliable")

    Returns:
        VerificationResult with status, certificate, counterexample, timing

    Example:
        >>> prop = TemporalProperty(
        ...     operator=TemporalOperator.ALWAYS,
        ...     predicate="data_consistent"
        ... )
        >>> result = verifier.verify_property(prop, architecture)
        >>> print(f"Verified: {result.verified}")

    References:
    - TD Commons: Property verification algorithm
    - Z3: SMT solving and model extraction
    """
    assumptions = assumptions or []

    # Check cache first
    if self.enable_cache:
        cached = self.cache.get(property, architecture)
        if cached is not None:
            return cached

    # Start timing
    start_time = time.time()

    try:
        # Create Z3 solver
        solver = z3.Solver()
        solver.set("timeout", self.timeout)

        # Encode architecture as SMT constraints
        arch_constraints = self._encode_architecture(architecture)
        for constraint in arch_constraints:
            solver.add(constraint)

        # Encode property as SMT formula
        # For ALWAYS/EVENTUALLY, we use bounded model checking
        prop_constraint = self._encode_property(property, architecture)
        solver.add(prop_constraint)

        # Check satisfiability
        check_result = solver.check()

        # Compute execution time
        execution_time = time.time() - start_time

        # Process result
        if check_result == z3.sat:
            # Property is satisfiable - this means it CAN hold
            # For ALWAYS properties, satisfiability means PROVED
            # For EVENTUALLY, it means we found a path
            status = VerificationStatus.PROVED
            counterexample = None

            # Generate proof certificate
            certificate = ProofCertificate(
                property_hash=property.hash(),
                architecture_hash=architecture.hash(),
                status=status,
                proof_steps=[],  # Z3 doesn't expose proof steps easily
                assumptions=assumptions,
                solver_version=get_z3_version()
            )

        elif check_result == z3.unsat:
            # Property is unsatisfiable - cannot hold
            status = VerificationStatus.DISPROVED
            counterexample = self._extract_counterexample(solver)
            certificate = None

        elif check_result == z3.unknown:
            # Solver couldn't determine (incomplete theory, heuristics failed)
            reason = solver.reason_unknown()
            if "timeout" in reason.lower():
                status = VerificationStatus.TIMEOUT
            else:
                status = VerificationStatus.UNKNOWN
            counterexample = None
            certificate = None

        else:
            # Unexpected result
            status = VerificationStatus.ERROR
            counterexample = None
            certificate = None

        # Create result
        result = VerificationResult(
            property=property,
            status=status,
            certificate=certificate,
            counterexample=counterexample,
            execution_time=execution_time,
            cached=False
        )

        # Cache result
        if self.enable_cache:
            self.cache.put(property, architecture, result)

        return result

    except Exception as e:
        # Handle errors gracefully
        execution_time = time.time() - start_time
        return VerificationResult(
            property=property,
            status=VerificationStatus.ERROR,
            certificate=None,
            counterexample={"error": str(e)},
            execution_time=execution_time,
            cached=False
        )

verify_specification(upir)

Verify all properties in a UPIR specification.

Verifies both invariants and properties from the formal specification against the architecture. Returns results for all properties.

Parameters:

Name	Type	Description	Default
upir	UPIR	UPIR instance with specification and architecture	required

Returns:

Type	Description
List[VerificationResult]	List of VerificationResult, one per property

Raises:

Type	Description
ValueError	If UPIR is missing specification or architecture

Example

upir = UPIR(...) upir.specification = FormalSpecification(...) upir.architecture = Architecture(...) results = verifier.verify_specification(upir) verified_count = sum(1 for r in results if r.verified) print(f"Verified {verified_count}/{len(results)} properties")

References: - TD Commons: Specification verification workflow

Source code in upir/verification/verifier.py

def verify_specification(self, upir: UPIR) -> List[VerificationResult]:
    """
    Verify all properties in a UPIR specification.

    Verifies both invariants and properties from the formal specification
    against the architecture. Returns results for all properties.

    Args:
        upir: UPIR instance with specification and architecture

    Returns:
        List of VerificationResult, one per property

    Raises:
        ValueError: If UPIR is missing specification or architecture

    Example:
        >>> upir = UPIR(...)
        >>> upir.specification = FormalSpecification(...)
        >>> upir.architecture = Architecture(...)
        >>> results = verifier.verify_specification(upir)
        >>> verified_count = sum(1 for r in results if r.verified)
        >>> print(f"Verified {verified_count}/{len(results)} properties")

    References:
    - TD Commons: Specification verification workflow
    """
    if upir.specification is None:
        raise ValueError("UPIR must have a specification to verify")
    if upir.architecture is None:
        raise ValueError("UPIR must have an architecture to verify")

    results = []

    # Verify invariants
    for invariant in upir.specification.invariants:
        result = self.verify_property(
            property=invariant,
            architecture=upir.architecture,
            assumptions=upir.specification.assumptions
        )
        results.append(result)

    # Verify properties
    for property in upir.specification.properties:
        result = self.verify_property(
            property=property,
            architecture=upir.architecture,
            assumptions=upir.specification.assumptions
        )
        results.append(result)

    return results

verify_incremental(upir, changed_properties)

Incrementally verify only changed properties, using cache for rest.

Per TD Commons disclosure, incremental verification is critical for performance when iterating on architectures. Only changed properties are re-verified; unchanged properties use cached results when available.

This method: 1. Invalidates cache if architecture changed (detects by hash) 2. Re-verifies changed properties (forced verification) 3. Uses cache for unchanged properties (may still miss if not cached) 4. Logs cache statistics at INFO level

Parameters:

Name	Type	Description	Default
upir	UPIR	UPIR instance with specification and architecture	required
changed_properties	Set[str]	Set of predicate names that changed (e.g., {"data_consistent", "backup_complete"})	required

Returns:

Type	Description
List[VerificationResult]	List of VerificationResult for all properties (invariants + properties)

Raises:

Type	Description
ValueError	If UPIR is missing specification or architecture

Example

Initial verification (all cache misses)

upir = UPIR(...) upir.specification = FormalSpecification( ... properties=[ ... TemporalProperty(ALWAYS, "data_consistent"), ... TemporalProperty(EVENTUALLY, "backup_complete"), ... TemporalProperty(WITHIN, "response_fast", time_bound=1.0) ... ] ... ) upir.architecture = Architecture(...) verifier = Verifier(enable_cache=True)

First verification - all misses

results = verifier.verify_incremental(upir, set())

INFO: Cache statistics: 0 hits, 3 misses, hit rate: 0.0%

assert verifier.cache.misses == 3 assert verifier.cache.hits == 0

Second verification with one change - 2 hits, 1 miss

results = verifier.verify_incremental( ... upir, ... changed_properties={"backup_complete"} ... )

INFO: Cache statistics: 2 hits, 4 misses, hit rate: 33.3%

assert verifier.cache.hits == 2 # data_consistent, response_fast assert verifier.cache.misses == 4 # 3 initial + 1 for backup_complete

Third verification with no changes - 3 hits, 0 new misses

results = verifier.verify_incremental(upir, set())

INFO: Cache statistics: 5 hits, 4 misses, hit rate: 55.6%

assert verifier.cache.hit_rate() > 50.0

References: - TD Commons: Incremental verification section - Cache invalidation on architecture changes

Source code in upir/verification/verifier.py

def verify_incremental(
    self,
    upir: UPIR,
    changed_properties: Set[str]
) -> List[VerificationResult]:
    """
    Incrementally verify only changed properties, using cache for rest.

    Per TD Commons disclosure, incremental verification is critical for
    performance when iterating on architectures. Only changed properties
    are re-verified; unchanged properties use cached results when available.

    This method:
    1. Invalidates cache if architecture changed (detects by hash)
    2. Re-verifies changed properties (forced verification)
    3. Uses cache for unchanged properties (may still miss if not cached)
    4. Logs cache statistics at INFO level

    Args:
        upir: UPIR instance with specification and architecture
        changed_properties: Set of predicate names that changed
                          (e.g., {"data_consistent", "backup_complete"})

    Returns:
        List of VerificationResult for all properties (invariants + properties)

    Raises:
        ValueError: If UPIR is missing specification or architecture

    Example:
        >>> # Initial verification (all cache misses)
        >>> upir = UPIR(...)
        >>> upir.specification = FormalSpecification(
        ...     properties=[
        ...         TemporalProperty(ALWAYS, "data_consistent"),
        ...         TemporalProperty(EVENTUALLY, "backup_complete"),
        ...         TemporalProperty(WITHIN, "response_fast", time_bound=1.0)
        ...     ]
        ... )
        >>> upir.architecture = Architecture(...)
        >>> verifier = Verifier(enable_cache=True)
        >>>
        >>> # First verification - all misses
        >>> results = verifier.verify_incremental(upir, set())
        >>> # INFO: Cache statistics: 0 hits, 3 misses, hit rate: 0.0%
        >>> assert verifier.cache.misses == 3
        >>> assert verifier.cache.hits == 0
        >>>
        >>> # Second verification with one change - 2 hits, 1 miss
        >>> results = verifier.verify_incremental(
        ...     upir,
        ...     changed_properties={"backup_complete"}
        ... )
        >>> # INFO: Cache statistics: 2 hits, 4 misses, hit rate: 33.3%
        >>> assert verifier.cache.hits == 2  # data_consistent, response_fast
        >>> assert verifier.cache.misses == 4  # 3 initial + 1 for backup_complete
        >>>
        >>> # Third verification with no changes - 3 hits, 0 new misses
        >>> results = verifier.verify_incremental(upir, set())
        >>> # INFO: Cache statistics: 5 hits, 4 misses, hit rate: 55.6%
        >>> assert verifier.cache.hit_rate() > 50.0

    References:
    - TD Commons: Incremental verification section
    - Cache invalidation on architecture changes
    """
    if upir.specification is None:
        raise ValueError("UPIR must have a specification to verify")
    if upir.architecture is None:
        raise ValueError("UPIR must have an architecture to verify")

    # Track previous architecture hash to detect changes
    # (In production, could store this in UPIR or verifier state)
    current_arch_hash = upir.architecture.hash()

    # Invalidate cache entries for changed properties
    if self.enable_cache and changed_properties:
        # Remove cache entries for changed properties
        # We need to recompute cache keys for changed properties
        all_props = list(upir.specification.invariants) + list(upir.specification.properties)
        for prop in all_props:
            if prop.predicate in changed_properties:
                cache_key = self.cache._compute_key(prop, upir.architecture)
                if cache_key in self.cache.cache:
                    del self.cache.cache[cache_key]

    results = []

    # Verify invariants
    # verify_property will check cache; changed properties were invalidated above
    for invariant in upir.specification.invariants:
        result = self.verify_property(
            property=invariant,
            architecture=upir.architecture,
            assumptions=upir.specification.assumptions
        )
        results.append(result)

    # Verify properties
    for property in upir.specification.properties:
        result = self.verify_property(
            property=property,
            architecture=upir.architecture,
            assumptions=upir.specification.assumptions
        )
        results.append(result)

    # Log cache statistics
    if self.enable_cache:
        logger.info(
            f"Cache statistics: {self.cache.hits} hits, "
            f"{self.cache.misses} misses, "
            f"hit rate: {self.cache.hit_rate():.1f}%"
        )

    return results

__str__()

Human-readable representation.

Source code in upir/verification/verifier.py

def __str__(self) -> str:
    """Human-readable representation."""
    cache_info = str(self.cache) if self.enable_cache else "disabled"
    return (
        f"Verifier(timeout={self.timeout}ms, "
        f"cache={cache_info})"
    )

---

Usage Example

from upir import UPIR, FormalSpecification, Architecture
from upir.verification.verifier import Verifier
from upir.verification.solver import VerificationStatus

# Create UPIR instance
upir = UPIR(specification=spec, architecture=arch)

# Create verifier
verifier = Verifier(timeout_ms=10000)

# Verify specification
results = verifier.verify_specification(upir)

# Check results
if results.status == VerificationStatus.PROVED:
    print(f"✓ Verified! {len(results.proved_properties)} properties proved")
    print(f"Time: {results.total_time_ms:.2f}ms")
elif results.status == VerificationStatus.FAILED:
    print(f"✗ Failed!")
    for counterexample in results.counterexamples:
        print(f"  Counterexample: {counterexample}")
elif results.status == VerificationStatus.UNKNOWN:
    print("? Unknown (timeout or incomplete)")

---

Incremental Verification

The verifier caches proven properties:

# First verification
results1 = verifier.verify_specification(upir)  # ~100ms

# Modify architecture slightly
upir.architecture.components[0]["latency_ms"] += 1

# Second verification (uses cached proofs)
results2 = verifier.verify_specification(upir)  # ~10ms

---

See Also

• SMT Solver - Low-level SMT solving
• FormalSpecification - Create specifications