pyfcstm.verify.taxonomy

Formal verification algorithm taxonomy for pyfcstm.

This module defines the metadata contract used by pyfcstm.verify to classify verification algorithms before they are implemented or wired into diagnostics. The taxonomy is intentionally independent from pyfcstm.diagnostics so raw verification metadata can evolve without depending on the inspect surface.

Example:

>>> from pyfcstm.verify.taxonomy import VerifyAlgorithmMeta
>>> meta = VerifyAlgorithmMeta(
...     name="demo",
...     description="Demo metadata.",
...     closedness="closed",
...     complexity_tier="structural",
...     smt_logic=None,
...     formula_size_scaling="none",
...     call_count_scaling="one",
...     incremental=False,
...     fallback_unknown_risk="none",
...     recommended_tactic=None,
...     quantifier_alternation_depth=0,
...     max_bitwidth=None,
...     theory_combination=(),
...     verification_scope="topological_only",
...     dominant_dim=("states",),
...     diagnostic_codes=(),
...     impl=None,
... )
>>> meta.name, meta.closedness
('demo', 'closed')

Closedness

pyfcstm.verify.taxonomy.Closedness: alias of Literal[‘closed’, ‘queried’]

ComplexityTier

pyfcstm.verify.taxonomy.ComplexityTier: alias of Literal[‘structural’, ‘smt_linear’, ‘smt_nonlinear_decidable’, ‘smt_undecidable_heuristic’, ‘bmc_search’]

SMTLogic

pyfcstm.verify.taxonomy.SMTLogic: alias of Literal[‘QF_UF’, ‘QF_LIA’, ‘QF_LRA’, ‘QF_LIRA’, ‘QF_UFLIA’, ‘QF_UFLRA’, ‘QF_BV’, ‘QF_FP’, ‘QF_NIA’, ‘QF_NRA’, ‘QF_UFNRA’, ‘QF_NIRA’, ‘transcendental’]

FormulaSizeScaling

pyfcstm.verify.taxonomy.FormulaSizeScaling: alias of Literal[‘none’, ‘constant’, ‘linear’, ‘quadratic’, ‘exponential_in_bitwidth’, ‘exponential_in_vars’, ‘doubly_exponential’]

CallCountScaling

pyfcstm.verify.taxonomy.CallCountScaling: alias of Literal[‘none’, ‘one’, ‘linear_in_states’, ‘linear_in_transitions’, ‘linear_in_vars’, ‘linear_in_leaves’, ‘quadratic_in_outgoing_per_state’, ‘quadratic_in_states’, ‘vars_times_transitions’, ‘k_unrollings’, ‘k_unrollings_times_branching’]

FallbackUnknownRisk

pyfcstm.verify.taxonomy.FallbackUnknownRisk: alias of Literal[‘none’, ‘low’, ‘medium’, ‘high’, ‘guaranteed_possible’]

VerificationScope

pyfcstm.verify.taxonomy.VerificationScope: alias of Literal[‘topological_only’, ‘smt_local’, ‘bmc_unrolled’]

COMPLEXITY_TIER_ORDER

pyfcstm.verify.taxonomy.COMPLEXITY_TIER_ORDER = ('structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic')

Built-in immutable sequence.

If no argument is given, the constructor returns an empty tuple. If iterable is specified the tuple is initialized from iterable’s items.

If the argument is a tuple, the return value is the same object.

CALL_COUNT_SCALING_ORDER

pyfcstm.verify.taxonomy.CALL_COUNT_SCALING_ORDER = ('none', 'one', 'linear_in_states', 'linear_in_transitions', 'linear_in_vars', 'linear_in_leaves', 'quadratic_in_outgoing_per_state', 'quadratic_in_states', 'vars_times_transitions')

Built-in immutable sequence.

If no argument is given, the constructor returns an empty tuple. If iterable is specified the tuple is initialized from iterable’s items.

If the argument is a tuple, the return value is the same object.

all

pyfcstm.verify.taxonomy.__all__ = ['CALL_COUNT_SCALING_ORDER', 'COMPLEXITY_TIER_ORDER', 'CallCountScaling', 'Closedness', 'ComplexityTier', 'FallbackUnknownRisk', 'FormulaSizeScaling', 'SMTLogic', 'VerificationScope', 'VerifyAlgorithmMeta']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

VerifyAlgorithmMeta

class pyfcstm.verify.taxonomy.VerifyAlgorithmMeta(name: str, description: str, closedness: Literal['closed', 'queried'], complexity_tier: Literal['structural', 'smt_linear', 'smt_nonlinear_decidable', 'smt_undecidable_heuristic', 'bmc_search'], smt_logic: Literal['QF_UF', 'QF_LIA', 'QF_LRA', 'QF_LIRA', 'QF_UFLIA', 'QF_UFLRA', 'QF_BV', 'QF_FP', 'QF_NIA', 'QF_NRA', 'QF_UFNRA', 'QF_NIRA', 'transcendental'] | None, formula_size_scaling: Literal['none', 'constant', 'linear', 'quadratic', 'exponential_in_bitwidth', 'exponential_in_vars', 'doubly_exponential'], call_count_scaling: Literal['none', 'one', 'linear_in_states', 'linear_in_transitions', 'linear_in_vars', 'linear_in_leaves', 'quadratic_in_outgoing_per_state', 'quadratic_in_states', 'vars_times_transitions', 'k_unrollings', 'k_unrollings_times_branching'], incremental: bool, fallback_unknown_risk: Literal['none', 'low', 'medium', 'high', 'guaranteed_possible'], recommended_tactic: str | None, quantifier_alternation_depth: int, max_bitwidth: int | None, theory_combination: Tuple[str, ...], verification_scope: Literal['topological_only', 'smt_local', 'bmc_unrolled'] | None, dominant_dim: Tuple[str, ...], diagnostic_codes: Tuple[str, ...], impl: Callable | None)[source]

Metadata describing one verification algorithm.

Parameters:

name (str) – Stable registry key and public algorithm name.
description (str) – Short human-readable algorithm summary.
closedness (Closedness) – Whether the algorithm can run without an explicit query.
complexity_tier (ComplexityTier) – Engineering complexity tier used by inspect gating.
smt_logic (Optional[SMTLogic]) – SMT-LIB logic family, or None for structural algorithms.
formula_size_scaling (FormulaSizeScaling) – Size growth of each generated formula.
call_count_scaling (CallCountScaling) – Number of algorithm or solver calls over model size.
incremental (bool) – Whether the implementation is expected to reuse solver state.
fallback_unknown_risk (FallbackUnknownRisk) – Risk that the algorithm must return inconclusive.
recommended_tactic (Optional[str]) – Z3 tactic name, or None when no solver is used.
quantifier_alternation_depth (int) – Quantifier alternation depth of formulas.
max_bitwidth (Optional[int]) – Maximum fixed bit-width if applicable, otherwise None.
theory_combination (Tuple[str, ...]) – SMT theory names combined by the algorithm.
verification_scope (Optional[VerificationScope]) – Boundary label for downstream result consumers.
dominant_dim (Tuple[str, ...]) – Dominant model dimensions for cost explanations.
diagnostic_codes (Tuple[str, ...]) – Diagnostics the algorithm may emit when integrated.
impl (Optional[Callable]) – Implementation callable, or None while the algorithm is pending.