SMT Solver¶

Low-level SMT solving with Z3.

Overview¶

The SMT solver module provides:

SMTVerifier: Low-level Z3 integration
VerificationResult: Verification results
VerificationStatus: Result status enum

Class Documentation¶

`upir.verification.solver.VerificationStatus` ¶

Bases: Enum

Status of a formal verification attempt.

Based on standard SMT solver result categories. Verification can: - PROVED: Property definitely holds (satisfiable/valid) - DISPROVED: Property definitely does not hold (counterexample found) - UNKNOWN: Solver cannot determine (incomplete theory, heuristics failed) - TIMEOUT: Verification exceeded time limit - ERROR: Internal error during verification

References: - SMT-LIB standard: Standard result categories - Z3 solver results: sat, unsat, unknown

Source code in upir/verification/solver.py

class VerificationStatus(Enum):
    """
    Status of a formal verification attempt.

    Based on standard SMT solver result categories. Verification can:
    - PROVED: Property definitely holds (satisfiable/valid)
    - DISPROVED: Property definitely does not hold (counterexample found)
    - UNKNOWN: Solver cannot determine (incomplete theory, heuristics failed)
    - TIMEOUT: Verification exceeded time limit
    - ERROR: Internal error during verification

    References:
    - SMT-LIB standard: Standard result categories
    - Z3 solver results: sat, unsat, unknown
    """
    PROVED = "PROVED"
    DISPROVED = "DISPROVED"
    UNKNOWN = "UNKNOWN"
    TIMEOUT = "TIMEOUT"
    ERROR = "ERROR"

`upir.verification.solver.VerificationResult` `dataclass` ¶

Result of verifying a temporal property against an architecture.

Verification results capture everything needed to understand whether a property holds, including the property itself, verification status, optional proof certificate, counterexamples if disproved, and metadata.

Based on TD Commons disclosure, verification results enable: - Decision making: Is this architecture safe? - Debugging: Why did verification fail? (counterexample) - Caching: Avoid re-verifying (cached flag) - Provenance: What was proved and when? (certificate)

Attributes:

Name	Type	Description
`property`	`TemporalProperty`	The temporal property that was verified
`status`	`VerificationStatus`	Verification status (PROVED, DISPROVED, etc.)
`certificate`	`Optional[ProofCertificate]`	Optional proof certificate for PROVED results
`counterexample`	`Optional[Dict[str, Any]]`	Optional counterexample for DISPROVED results
`execution_time`	`float`	Time taken for verification (seconds)
`cached`	`bool`	Whether result came from cache (not freshly computed)

Example

result = VerificationResult( ... property=TemporalProperty(...), ... status=VerificationStatus.PROVED, ... certificate=ProofCertificate(...), ... counterexample=None, ... execution_time=1.23, ... cached=False ... ) result.verified True

References: - TD Commons: Verification result structure - SMT solving: Standard result format (status + model/proof)

Source code in upir/verification/solver.py

@dataclass
class VerificationResult:
    """
    Result of verifying a temporal property against an architecture.

    Verification results capture everything needed to understand whether
    a property holds, including the property itself, verification status,
    optional proof certificate, counterexamples if disproved, and metadata.

    Based on TD Commons disclosure, verification results enable:
    - Decision making: Is this architecture safe?
    - Debugging: Why did verification fail? (counterexample)
    - Caching: Avoid re-verifying (cached flag)
    - Provenance: What was proved and when? (certificate)

    Attributes:
        property: The temporal property that was verified
        status: Verification status (PROVED, DISPROVED, etc.)
        certificate: Optional proof certificate for PROVED results
        counterexample: Optional counterexample for DISPROVED results
        execution_time: Time taken for verification (seconds)
        cached: Whether result came from cache (not freshly computed)

    Example:
        >>> result = VerificationResult(
        ...     property=TemporalProperty(...),
        ...     status=VerificationStatus.PROVED,
        ...     certificate=ProofCertificate(...),
        ...     counterexample=None,
        ...     execution_time=1.23,
        ...     cached=False
        ... )
        >>> result.verified
        True

    References:
    - TD Commons: Verification result structure
    - SMT solving: Standard result format (status + model/proof)
    """
    property: TemporalProperty
    status: VerificationStatus
    certificate: Optional[ProofCertificate] = None
    counterexample: Optional[Dict[str, Any]] = None
    execution_time: float = 0.0
    cached: bool = False

    @property
    def verified(self) -> bool:
        """
        Check if property was successfully verified (proved).

        Returns:
            True if status is PROVED, False otherwise

        Example:
            >>> result = VerificationResult(
            ...     property=TemporalProperty(...),
            ...     status=VerificationStatus.PROVED,
            ...     execution_time=1.0
            ... )
            >>> result.verified
            True
            >>> result2 = VerificationResult(
            ...     property=TemporalProperty(...),
            ...     status=VerificationStatus.UNKNOWN,
            ...     execution_time=1.0
            ... )
            >>> result2.verified
            False
        """
        return self.status == VerificationStatus.PROVED

    def to_dict(self) -> Dict[str, Any]:
        """
        Serialize verification result to JSON-compatible dictionary.

        Returns:
            Dictionary with all result fields

        Example:
            >>> result = VerificationResult(
            ...     property=TemporalProperty(...),
            ...     status=VerificationStatus.PROVED,
            ...     execution_time=1.23
            ... )
            >>> d = result.to_dict()
            >>> d["status"]
            'PROVED'
        """
        return {
            "property": self.property.to_dict(),
            "status": self.status.value,
            "certificate": (
                self.certificate.to_dict() if self.certificate else None
            ),
            "counterexample": self.counterexample,
            "execution_time": self.execution_time,
            "cached": self.cached
        }

    @classmethod
    def from_dict(cls, data: Dict[str, Any]) -> "VerificationResult":
        """
        Deserialize verification result from dictionary.

        Args:
            data: Dictionary containing result fields

        Returns:
            VerificationResult instance

        Example:
            >>> data = {
            ...     "property": {...},
            ...     "status": "PROVED",
            ...     "certificate": None,
            ...     "counterexample": None,
            ...     "execution_time": 1.23,
            ...     "cached": False
            ... }
            >>> result = VerificationResult.from_dict(data)
            >>> result.status == VerificationStatus.PROVED
            True
        """
        return cls(
            property=TemporalProperty.from_dict(data["property"]),
            status=VerificationStatus(data["status"]),
            certificate=(
                ProofCertificate.from_dict(data["certificate"])
                if data.get("certificate") else None
            ),
            counterexample=data.get("counterexample"),
            execution_time=data.get("execution_time", 0.0),
            cached=data.get("cached", False)
        )

    def __str__(self) -> str:
        """Human-readable string representation."""
        parts = [
            f"VerificationResult({self.status.value}",
            f"property={self.property.predicate}",
        ]
        if self.cached:
            parts.append("cached=True")
        if self.execution_time > 0:
            parts.append(f"time={self.execution_time:.3f}s")

        return ", ".join(parts) + ")"

    def __repr__(self) -> str:
        """Developer-friendly representation."""
        return (
            f"VerificationResult(status={self.status.value}, "
            f"property={self.property.predicate}, "
            f"verified={self.verified}, "
            f"cached={self.cached})"
        )

Functions¶

`verified()` ¶

Check if property was successfully verified (proved).

Returns:

Type	Description
`bool`	True if status is PROVED, False otherwise

Example

result = VerificationResult( ... property=TemporalProperty(...), ... status=VerificationStatus.PROVED, ... execution_time=1.0 ... ) result.verified True result2 = VerificationResult( ... property=TemporalProperty(...), ... status=VerificationStatus.UNKNOWN, ... execution_time=1.0 ... ) result2.verified False

Source code in upir/verification/solver.py

@property
def verified(self) -> bool:
    """
    Check if property was successfully verified (proved).

    Returns:
        True if status is PROVED, False otherwise

    Example:
        >>> result = VerificationResult(
        ...     property=TemporalProperty(...),
        ...     status=VerificationStatus.PROVED,
        ...     execution_time=1.0
        ... )
        >>> result.verified
        True
        >>> result2 = VerificationResult(
        ...     property=TemporalProperty(...),
        ...     status=VerificationStatus.UNKNOWN,
        ...     execution_time=1.0
        ... )
        >>> result2.verified
        False
    """
    return self.status == VerificationStatus.PROVED

`to_dict()` ¶

Serialize verification result to JSON-compatible dictionary.

Returns:

Type	Description
`Dict[str, Any]`	Dictionary with all result fields

Example

result = VerificationResult( ... property=TemporalProperty(...), ... status=VerificationStatus.PROVED, ... execution_time=1.23 ... ) d = result.to_dict() d["status"] 'PROVED'

Source code in upir/verification/solver.py

def to_dict(self) -> Dict[str, Any]:
    """
    Serialize verification result to JSON-compatible dictionary.

    Returns:
        Dictionary with all result fields

    Example:
        >>> result = VerificationResult(
        ...     property=TemporalProperty(...),
        ...     status=VerificationStatus.PROVED,
        ...     execution_time=1.23
        ... )
        >>> d = result.to_dict()
        >>> d["status"]
        'PROVED'
    """
    return {
        "property": self.property.to_dict(),
        "status": self.status.value,
        "certificate": (
            self.certificate.to_dict() if self.certificate else None
        ),
        "counterexample": self.counterexample,
        "execution_time": self.execution_time,
        "cached": self.cached
    }

`from_dict(data)` `classmethod` ¶

Deserialize verification result from dictionary.

Parameters:

Name	Type	Description	Default
`data`	`Dict[str, Any]`	Dictionary containing result fields	required

Returns:

Type	Description
`VerificationResult`	VerificationResult instance

Example

data = { ... "property": {...}, ... "status": "PROVED", ... "certificate": None, ... "counterexample": None, ... "execution_time": 1.23, ... "cached": False ... } result = VerificationResult.from_dict(data) result.status == VerificationStatus.PROVED True

Source code in upir/verification/solver.py

@classmethod
def from_dict(cls, data: Dict[str, Any]) -> "VerificationResult":
    """
    Deserialize verification result from dictionary.

    Args:
        data: Dictionary containing result fields

    Returns:
        VerificationResult instance

    Example:
        >>> data = {
        ...     "property": {...},
        ...     "status": "PROVED",
        ...     "certificate": None,
        ...     "counterexample": None,
        ...     "execution_time": 1.23,
        ...     "cached": False
        ... }
        >>> result = VerificationResult.from_dict(data)
        >>> result.status == VerificationStatus.PROVED
        True
    """
    return cls(
        property=TemporalProperty.from_dict(data["property"]),
        status=VerificationStatus(data["status"]),
        certificate=(
            ProofCertificate.from_dict(data["certificate"])
            if data.get("certificate") else None
        ),
        counterexample=data.get("counterexample"),
        execution_time=data.get("execution_time", 0.0),
        cached=data.get("cached", False)
    )

`str()` ¶

Human-readable string representation.

Source code in upir/verification/solver.py

def __str__(self) -> str:
    """Human-readable string representation."""
    parts = [
        f"VerificationResult({self.status.value}",
        f"property={self.property.predicate}",
    ]
    if self.cached:
        parts.append("cached=True")
    if self.execution_time > 0:
        parts.append(f"time={self.execution_time:.3f}s")

    return ", ".join(parts) + ")"

`repr()` ¶

Developer-friendly representation.

Source code in upir/verification/solver.py

def __repr__(self) -> str:
    """Developer-friendly representation."""
    return (
        f"VerificationResult(status={self.status.value}, "
        f"property={self.property.predicate}, "
        f"verified={self.verified}, "
        f"cached={self.cached})"
    )

`upir.verification.solver.ProofCertificate` `dataclass` ¶

A certificate attesting to a formal verification result.

Proof certificates provide cryptographically verifiable evidence that a property was (or was not) proved for a specific architecture at a specific time with specific assumptions.

Based on TD Commons disclosure, certificates enable: - Reproducibility: Same property + architecture should give same result - Auditability: Trace what was verified and when - Caching: Avoid re-proving same properties

Attributes:

Name	Type	Description
`property_hash`	`str`	SHA-256 hash of the temporal property
`architecture_hash`	`str`	SHA-256 hash of the architecture
`status`	`VerificationStatus`	Verification result status
`proof_steps`	`List[Dict[str, Any]]`	List of proof steps (solver-specific format)
`assumptions`	`List[str]`	List of assumptions made during proof
`timestamp`	`datetime`	When verification was performed (UTC)
`solver_version`	`str`	Version of solver used (e.g., "z3-4.12.2")

Example

cert = ProofCertificate( ... property_hash="abc123...", ... architecture_hash="def456...", ... status=VerificationStatus.PROVED, ... proof_steps=[{"step": 1, "action": "simplify"}], ... assumptions=["network_reliable"], ... timestamp=datetime.utcnow(), ... solver_version="z3-4.12.2" ... ) cert_hash = cert.generate_hash()

References: - TD Commons: Proof certificate structure - Cryptographic certificates: SHA-256 for integrity

Source code in upir/verification/solver.py

@dataclass
class ProofCertificate:
    """
    A certificate attesting to a formal verification result.

    Proof certificates provide cryptographically verifiable evidence that
    a property was (or was not) proved for a specific architecture at
    a specific time with specific assumptions.

    Based on TD Commons disclosure, certificates enable:
    - Reproducibility: Same property + architecture should give same result
    - Auditability: Trace what was verified and when
    - Caching: Avoid re-proving same properties

    Attributes:
        property_hash: SHA-256 hash of the temporal property
        architecture_hash: SHA-256 hash of the architecture
        status: Verification result status
        proof_steps: List of proof steps (solver-specific format)
        assumptions: List of assumptions made during proof
        timestamp: When verification was performed (UTC)
        solver_version: Version of solver used (e.g., "z3-4.12.2")

    Example:
        >>> cert = ProofCertificate(
        ...     property_hash="abc123...",
        ...     architecture_hash="def456...",
        ...     status=VerificationStatus.PROVED,
        ...     proof_steps=[{"step": 1, "action": "simplify"}],
        ...     assumptions=["network_reliable"],
        ...     timestamp=datetime.utcnow(),
        ...     solver_version="z3-4.12.2"
        ... )
        >>> cert_hash = cert.generate_hash()

    References:
    - TD Commons: Proof certificate structure
    - Cryptographic certificates: SHA-256 for integrity
    """
    property_hash: str
    architecture_hash: str
    status: VerificationStatus
    proof_steps: List[Dict[str, Any]] = field(default_factory=list)
    assumptions: List[str] = field(default_factory=list)
    timestamp: datetime = field(default_factory=datetime.utcnow)
    solver_version: str = Z3_VERSION

    def generate_hash(self) -> str:
        """
        Generate SHA-256 hash of this certificate for integrity verification.

        The hash is computed over all certificate fields (except the hash itself)
        in a deterministic way to enable verification that the certificate
        has not been tampered with.

        Returns:
            Hexadecimal SHA-256 hash string

        Example:
            >>> cert = ProofCertificate(
            ...     property_hash="abc",
            ...     architecture_hash="def",
            ...     status=VerificationStatus.PROVED,
            ...     timestamp=datetime(2024, 1, 1, 12, 0, 0),
            ...     solver_version="z3-4.12.2"
            ... )
            >>> hash1 = cert.generate_hash()
            >>> hash2 = cert.generate_hash()
            >>> hash1 == hash2  # Deterministic
            True

        References:
        - SHA-256: Industry standard cryptographic hash
        - Python hashlib: https://docs.python.org/3/library/hashlib.html
        """
        cert_dict = {
            "property_hash": self.property_hash,
            "architecture_hash": self.architecture_hash,
            "status": self.status.value,
            "proof_steps": self.proof_steps,
            "assumptions": sorted(self.assumptions),
            "timestamp": self.timestamp.isoformat(),
            "solver_version": self.solver_version
        }

        # Create deterministic JSON
        json_str = json.dumps(cert_dict, sort_keys=True)

        # Compute SHA-256
        hash_obj = hashlib.sha256(json_str.encode('utf-8'))
        return hash_obj.hexdigest()

    def to_dict(self) -> Dict[str, Any]:
        """
        Serialize proof certificate to JSON-compatible dictionary.

        Returns:
            Dictionary with all certificate fields

        Example:
            >>> cert = ProofCertificate(
            ...     property_hash="abc",
            ...     architecture_hash="def",
            ...     status=VerificationStatus.PROVED,
            ...     timestamp=datetime(2024, 1, 1, 12, 0, 0),
            ...     solver_version="z3-4.12.2"
            ... )
            >>> d = cert.to_dict()
            >>> d["status"]
            'PROVED'
        """
        return {
            "property_hash": self.property_hash,
            "architecture_hash": self.architecture_hash,
            "status": self.status.value,
            "proof_steps": self.proof_steps.copy(),
            "assumptions": self.assumptions.copy(),
            "timestamp": self.timestamp.isoformat(),
            "solver_version": self.solver_version
        }

    @classmethod
    def from_dict(cls, data: Dict[str, Any]) -> "ProofCertificate":
        """
        Deserialize proof certificate from dictionary.

        Args:
            data: Dictionary containing certificate fields

        Returns:
            ProofCertificate instance

        Example:
            >>> data = {
            ...     "property_hash": "abc",
            ...     "architecture_hash": "def",
            ...     "status": "PROVED",
            ...     "proof_steps": [],
            ...     "assumptions": [],
            ...     "timestamp": "2024-01-01T12:00:00",
            ...     "solver_version": "z3-4.12.2"
            ... }
            >>> cert = ProofCertificate.from_dict(data)
            >>> cert.status == VerificationStatus.PROVED
            True
        """
        return cls(
            property_hash=data["property_hash"],
            architecture_hash=data["architecture_hash"],
            status=VerificationStatus(data["status"]),
            proof_steps=data.get("proof_steps", []),
            assumptions=data.get("assumptions", []),
            timestamp=datetime.fromisoformat(data["timestamp"]),
            solver_version=data.get("solver_version", "unknown")
        )

    def __str__(self) -> str:
        """Human-readable string representation."""
        return (
            f"ProofCertificate({self.status.value}, "
            f"solver={self.solver_version})"
        )

Functions¶

`generate_hash()` ¶

Generate SHA-256 hash of this certificate for integrity verification.

The hash is computed over all certificate fields (except the hash itself) in a deterministic way to enable verification that the certificate has not been tampered with.

Returns:

Type	Description
`str`	Hexadecimal SHA-256 hash string

Example

cert = ProofCertificate( ... property_hash="abc", ... architecture_hash="def", ... status=VerificationStatus.PROVED, ... timestamp=datetime(2024, 1, 1, 12, 0, 0), ... solver_version="z3-4.12.2" ... ) hash1 = cert.generate_hash() hash2 = cert.generate_hash() hash1 == hash2 # Deterministic True

References: - SHA-256: Industry standard cryptographic hash - Python hashlib: https://docs.python.org/3/library/hashlib.html

Source code in upir/verification/solver.py

def generate_hash(self) -> str:
    """
    Generate SHA-256 hash of this certificate for integrity verification.

    The hash is computed over all certificate fields (except the hash itself)
    in a deterministic way to enable verification that the certificate
    has not been tampered with.

    Returns:
        Hexadecimal SHA-256 hash string

    Example:
        >>> cert = ProofCertificate(
        ...     property_hash="abc",
        ...     architecture_hash="def",
        ...     status=VerificationStatus.PROVED,
        ...     timestamp=datetime(2024, 1, 1, 12, 0, 0),
        ...     solver_version="z3-4.12.2"
        ... )
        >>> hash1 = cert.generate_hash()
        >>> hash2 = cert.generate_hash()
        >>> hash1 == hash2  # Deterministic
        True

    References:
    - SHA-256: Industry standard cryptographic hash
    - Python hashlib: https://docs.python.org/3/library/hashlib.html
    """
    cert_dict = {
        "property_hash": self.property_hash,
        "architecture_hash": self.architecture_hash,
        "status": self.status.value,
        "proof_steps": self.proof_steps,
        "assumptions": sorted(self.assumptions),
        "timestamp": self.timestamp.isoformat(),
        "solver_version": self.solver_version
    }

    # Create deterministic JSON
    json_str = json.dumps(cert_dict, sort_keys=True)

    # Compute SHA-256
    hash_obj = hashlib.sha256(json_str.encode('utf-8'))
    return hash_obj.hexdigest()

`to_dict()` ¶

Serialize proof certificate to JSON-compatible dictionary.

Returns:

Type	Description
`Dict[str, Any]`	Dictionary with all certificate fields

Example

cert = ProofCertificate( ... property_hash="abc", ... architecture_hash="def", ... status=VerificationStatus.PROVED, ... timestamp=datetime(2024, 1, 1, 12, 0, 0), ... solver_version="z3-4.12.2" ... ) d = cert.to_dict() d["status"] 'PROVED'

Source code in upir/verification/solver.py

def to_dict(self) -> Dict[str, Any]:
    """
    Serialize proof certificate to JSON-compatible dictionary.

    Returns:
        Dictionary with all certificate fields

    Example:
        >>> cert = ProofCertificate(
        ...     property_hash="abc",
        ...     architecture_hash="def",
        ...     status=VerificationStatus.PROVED,
        ...     timestamp=datetime(2024, 1, 1, 12, 0, 0),
        ...     solver_version="z3-4.12.2"
        ... )
        >>> d = cert.to_dict()
        >>> d["status"]
        'PROVED'
    """
    return {
        "property_hash": self.property_hash,
        "architecture_hash": self.architecture_hash,
        "status": self.status.value,
        "proof_steps": self.proof_steps.copy(),
        "assumptions": self.assumptions.copy(),
        "timestamp": self.timestamp.isoformat(),
        "solver_version": self.solver_version
    }

`from_dict(data)` `classmethod` ¶

Deserialize proof certificate from dictionary.

Parameters:

Name	Type	Description	Default
`data`	`Dict[str, Any]`	Dictionary containing certificate fields	required

Returns:

Type	Description
`ProofCertificate`	ProofCertificate instance

Example

data = { ... "property_hash": "abc", ... "architecture_hash": "def", ... "status": "PROVED", ... "proof_steps": [], ... "assumptions": [], ... "timestamp": "2024-01-01T12:00:00", ... "solver_version": "z3-4.12.2" ... } cert = ProofCertificate.from_dict(data) cert.status == VerificationStatus.PROVED True

Source code in upir/verification/solver.py

@classmethod
def from_dict(cls, data: Dict[str, Any]) -> "ProofCertificate":
    """
    Deserialize proof certificate from dictionary.

    Args:
        data: Dictionary containing certificate fields

    Returns:
        ProofCertificate instance

    Example:
        >>> data = {
        ...     "property_hash": "abc",
        ...     "architecture_hash": "def",
        ...     "status": "PROVED",
        ...     "proof_steps": [],
        ...     "assumptions": [],
        ...     "timestamp": "2024-01-01T12:00:00",
        ...     "solver_version": "z3-4.12.2"
        ... }
        >>> cert = ProofCertificate.from_dict(data)
        >>> cert.status == VerificationStatus.PROVED
        True
    """
    return cls(
        property_hash=data["property_hash"],
        architecture_hash=data["architecture_hash"],
        status=VerificationStatus(data["status"]),
        proof_steps=data.get("proof_steps", []),
        assumptions=data.get("assumptions", []),
        timestamp=datetime.fromisoformat(data["timestamp"]),
        solver_version=data.get("solver_version", "unknown")
    )

`str()` ¶

Human-readable string representation.

Source code in upir/verification/solver.py

def __str__(self) -> str:
    """Human-readable string representation."""
    return (
        f"ProofCertificate({self.status.value}, "
        f"solver={self.solver_version})"
    )

SMT Solver¶

Overview¶

Class Documentation¶

upir.verification.solver.VerificationStatus ¶

upir.verification.solver.VerificationResult dataclass ¶

Functions¶

verified() ¶

to_dict() ¶

from_dict(data) classmethod ¶

__str__() ¶

__repr__() ¶

upir.verification.solver.ProofCertificate dataclass ¶

Functions¶

generate_hash() ¶

to_dict() ¶

from_dict(data) classmethod ¶

__str__() ¶

See Also¶

`upir.verification.solver.VerificationStatus` ¶

`upir.verification.solver.VerificationResult` `dataclass` ¶

`verified()` ¶

`to_dict()` ¶

`from_dict(data)` `classmethod` ¶

`str()` ¶

`repr()` ¶

`upir.verification.solver.ProofCertificate` `dataclass` ¶

`generate_hash()` ¶

`to_dict()` ¶

`from_dict(data)` `classmethod` ¶

`str()` ¶