provably.decorators

from provably import verified, runtime_checked
from provably.decorators import VerificationError, ContractViolationError

---

@verified

Prove a function's pre/post contract using Z3 at decoration time. Attaches a ProofCertificate as fn.__proof__. No solver runs at call time. A thin functools.wraps wrapper is applied; check_contracts=True adds runtime contract checks.

@verified(
    pre=lambda a, b: b > 0,
    post=lambda a, b, result: (result >= 0) & (result < b),
)
def modulo(a: int, b: int) -> int:
    return a % b

modulo.__proof__.verified  # True
str(modulo.__proof__)      # "[Q.E.D.] modulo"

Parameter	Type	Default	Description
pre	Callable \| None	None	Precondition. Same params as function. Use &/\|/~.
post	Callable \| None	None	Postcondition. Params + result (last arg).
raise_on_failure	bool	False	Raise VerificationError if proof fails.
timeout_ms	int \| None	None	Per-proof Z3 timeout. Overrides configure().
contracts	dict \| None	None	Helper contracts for modular verification.
check_contracts	bool	False	Also enforce pre/post at runtime.

Use & not and in pre/post lambdas

and short-circuits and silently drops conjuncts. See Contracts.

---

@runtime_checked

Check pre/post at every call using Python evaluation. No Z3 required.

@runtime_checked(
    pre=lambda x: x >= 0,
    post=lambda x, result: result >= 0,
)
def sqrt_approx(x: float) -> float:
    return x ** 0.5

sqrt_approx(4.0)   # 2.0
sqrt_approx(-1.0)  # raises ContractViolationError

Parameter	Type	Default	Description
pre	Callable \| None	None	Precondition. Evaluated with actual arguments.
post	Callable \| None	None	Postcondition. Arguments + result.
raise_on_failure	bool	True	Raise ContractViolationError. If False, log warning.

---

VerificationError

Raised by @verified(raise_on_failure=True) when proof fails.

try:
    @verified(raise_on_failure=True, post=lambda x, result: result > x)
    def bad(x: int) -> int:
        return x
except VerificationError as e:
    e.certificate.counterexample  # {'x': 0, '__return__': 0}

---

ContractViolationError

Raised by @runtime_checked (or @verified(check_contracts=True)) on violation.

class ContractViolationError(Exception):
    kind:      str         # "pre" or "post"
    func_name: str
    args_:     tuple
    result:    Any | None  # set for "post" violations

---

provably.decorators

The @verified decorator — proof-carrying Python functions.

Usage::

from provably import verified
from provably.types import Ge
from typing import Annotated

# Bare decorator — proves refinement type annotations
@verified
def double(x: Annotated[float, Ge(0)]) -> Annotated[float, Ge(0)]:
    return x * 2

# With explicit pre/post contracts
@verified(
    pre=lambda x, lo, hi: lo <= hi,
    post=lambda x, lo, hi, result: (result >= lo) & (result <= hi),
)
def clamp(x: float, lo: float, hi: float) -> float:
    if x < lo:
        return lo
    elif x > hi:
        return hi
    else:
        return x

# Access proof certificate
clamp.__proof__  # ProofCertificate

# Runtime-only checking (no Z3 required)
@runtime_checked(
    pre=lambda x: x >= 0,
    post=lambda x, result: result >= 0,
)
def sqrt_approx(x: float) -> float:
    return x ** 0.5

In pre/post lambdas for @verified, use & instead of 'and',

| instead of 'or', ~ instead of 'not'. Python's boolean operators cannot be overloaded and will not produce Z3 expressions.

Classes

ContractViolationError

ContractViolationError(kind: str, func_name: str, args_: tuple[Any, ...], result: Any = None)

Bases: Exception

Raised by :func:runtime_checked when a contract is violated at runtime.

Attributes:

Name	Type	Description
kind		"pre" or "post".
args_		The positional arguments that triggered the violation.
result		The return value (only set when kind == "post").

Source code in src/provably/decorators.py

def __init__(
    self,
    kind: str,
    func_name: str,
    args_: tuple[Any, ...],
    result: Any = None,
) -> None:
    self.kind = kind
    self.func_name = func_name
    self.args_ = args_
    self.result = result
    if kind == "pre":
        msg = f"Precondition violated for '{func_name}' with args {args_}"
    else:
        msg = f"Postcondition violated for '{func_name}' with args {args_}, result={result!r}"
    super().__init__(msg)

VerificationError

VerificationError(certificate: ProofCertificate)

Bases: Exception

Raised when raise_on_failure=True and verification fails.

The failing :class:~provably.engine.ProofCertificate is available as exc.certificate.

Source code in src/provably/decorators.py

def __init__(self, certificate: ProofCertificate) -> None:
    self.certificate = certificate
    super().__init__(str(certificate))

Functions

runtime_checked

runtime_checked(func: F | None = None, *, pre: Callable[..., Any] | None = None, post: Callable[..., Any] | None = None, raise_on_failure: bool = True) -> F | Callable[[F], F]

Decorator that checks pre/post contracts at runtime without Z3.

Unlike :func:verified, this decorator does not perform a static proof. It simply evaluates the pre and post conditions on every actual call and raises :class:ContractViolationError when one fails.

This is useful when:

• You want zero solver overhead at runtime.
• The function body uses constructs the translator does not support.
• You want defence-in-depth in addition to a static proof.

Parameters:

Name	Type	Description	Default
func	F | None	The function (when used as bare @runtime_checked).	None
pre	Callable[..., Any] | None	Precondition callable — takes the same arguments as func. Must return a truthy value when the precondition holds.	None
post	Callable[..., Any] | None	Postcondition callable — takes (*args, result). Must return a truthy value when the postcondition holds.	None
raise_on_failure	bool	If True (default), raise :class:ContractViolationError on violation. If False, log a warning instead.	True

Returns:

Type	Description
F | Callable[[F], F]	The wrapped function. Identical to the original at call sites
F | Callable[[F], F]	when all contracts pass.

Example::

@runtime_checked(
    pre=lambda x: x >= 0,
    post=lambda x, result: result >= 0,
)
def sqrt_approx(x: float) -> float:
    return x ** 0.5

Source code in src/provably/decorators.py

def runtime_checked(
    func: F | None = None,
    *,
    pre: Callable[..., Any] | None = None,
    post: Callable[..., Any] | None = None,
    raise_on_failure: bool = True,
) -> F | Callable[[F], F]:
    """Decorator that checks pre/post contracts at runtime without Z3.

    Unlike :func:`verified`, this decorator does not perform a static proof.
    It simply evaluates the pre and post conditions on every actual call and
    raises :class:`ContractViolationError` when one fails.

    This is useful when:

    - You want zero solver overhead at runtime.
    - The function body uses constructs the translator does not support.
    - You want defence-in-depth in addition to a static proof.

    Args:
        func: The function (when used as bare ``@runtime_checked``).
        pre: Precondition callable — takes the same arguments as *func*.
            Must return a truthy value when the precondition holds.
        post: Postcondition callable — takes ``(*args, result)``.
            Must return a truthy value when the postcondition holds.
        raise_on_failure: If ``True`` (default), raise
            :class:`ContractViolationError` on violation.  If ``False``,
            log a warning instead.

    Returns:
        The wrapped function.  Identical to the original at call sites
        when all contracts pass.

    Example::

        @runtime_checked(
            pre=lambda x: x >= 0,
            post=lambda x, result: result >= 0,
        )
        def sqrt_approx(x: float) -> float:
            return x ** 0.5
    """
    if func is not None:
        return _runtime_wrap(func, pre, post, raise_on_failure)

    def decorator(fn: F) -> F:
        return _runtime_wrap(fn, pre, post, raise_on_failure)

    return decorator  # type: ignore[return-value]

verified

verified(func: F) -> F

verified(*, pre: Callable[..., Any] | None = ..., post: Callable[..., Any] | None = ..., raise_on_failure: bool = ..., strict: bool = ..., timeout_ms: int = ..., contracts: dict[str, dict[str, Any]] | None = ..., check_contracts: bool = ...) -> Callable[[F], F]

verified(func: F | None = None, *, pre: Callable[..., Any] | None = None, post: Callable[..., Any] | None = None, raise_on_failure: bool | None = None, strict: bool | None = None, timeout_ms: int | None = None, contracts: dict[str, dict[str, Any]] | None = None, check_contracts: bool = False) -> F | Callable[[F], F]

Decorator that formally verifies a Python function using Z3.

Parameters:

Name	Type	Description	Default
func	F | None	The function (when used as bare @verified).	None
pre	Callable[..., Any] | None	Precondition lambda — takes the same arguments as func. Use & / | / ~ instead of and / or / not to stay in Z3 expression space.	None
post	Callable[..., Any] | None	Postcondition lambda — takes (*args, result).	None
raise_on_failure	bool | None	If True, raise :class:VerificationError when the proof fails. Defaults to the global setting (False).	None
strict	bool | None	Deprecated alias for raise_on_failure. Will be removed in a future version.	None
timeout_ms	int | None	Z3 solver timeout in milliseconds. Defaults to the global setting (5000ms).	None
contracts	dict[str, dict[str, Any]] | None	Pre/post contracts of functions called inside func, keyed by function name. Enables modular verification.	None
check_contracts	bool	If True, the wrapper also performs a runtime pre/post check on every call (in addition to the static Z3 proof). Useful as a defence-in-depth measure for functions whose proof is SKIPPED or UNKNOWN.	False

Returns:

Type	Description
F | Callable[[F], F]	The original function, unchanged at runtime, with a
F | Callable[[F], F]	class:~provably.engine.ProofCertificate attached as
F | Callable[[F], F]	func.__proof__.

The decorated function is wrapped in a thin functools.wraps passthrough. No solver overhead at call time (unless check_contracts=True, which adds runtime contract checks).

Async functions are not translated (Z3 does not support coroutine bodies). They receive a SKIPPED certificate and the wrapper is a passthrough.

Source code in src/provably/decorators.py

def verified(
    func: F | None = None,
    *,
    pre: Callable[..., Any] | None = None,
    post: Callable[..., Any] | None = None,
    raise_on_failure: bool | None = None,
    strict: bool | None = None,
    timeout_ms: int | None = None,
    contracts: dict[str, dict[str, Any]] | None = None,
    check_contracts: bool = False,
) -> F | Callable[[F], F]:
    """Decorator that formally verifies a Python function using Z3.

    Args:
        func: The function (when used as bare ``@verified``).
        pre: Precondition lambda — takes the same arguments as *func*.
            Use ``&`` / ``|`` / ``~`` instead of ``and`` / ``or`` / ``not``
            to stay in Z3 expression space.
        post: Postcondition lambda — takes ``(*args, result)``.
        raise_on_failure: If ``True``, raise :class:`VerificationError` when
            the proof fails.  Defaults to the global setting (``False``).
        strict: Deprecated alias for *raise_on_failure*.  Will be removed in
            a future version.
        timeout_ms: Z3 solver timeout in milliseconds.  Defaults to the
            global setting (5000ms).
        contracts: Pre/post contracts of functions called inside *func*,
            keyed by function name.  Enables modular verification.
        check_contracts: If ``True``, the wrapper also performs a runtime
            pre/post check on every call (in addition to the static Z3 proof).
            Useful as a defence-in-depth measure for functions whose proof
            is SKIPPED or UNKNOWN.

    Returns:
        The original function, unchanged at runtime, with a
        :class:`~provably.engine.ProofCertificate` attached as
        ``func.__proof__``.

    The decorated function is wrapped in a thin ``functools.wraps``
    passthrough.  No solver overhead at call time (unless
    ``check_contracts=True``, which adds runtime contract checks).

    Async functions are not translated (Z3 does not support coroutine bodies).
    They receive a ``SKIPPED`` certificate and the wrapper is a passthrough.
    """
    # Handle deprecated 'strict' parameter
    if strict is not None:
        warnings.warn(
            "The 'strict' parameter is deprecated. Use 'raise_on_failure' instead.",
            DeprecationWarning,
            stacklevel=2,
        )
        if raise_on_failure is None:
            raise_on_failure = strict

    # Fall back to global config
    if raise_on_failure is None:
        raise_on_failure = bool(_config.get("raise_on_failure", False))
    if timeout_ms is None:
        timeout_ms = int(_config.get("timeout_ms", 5000))

    if func is not None:
        # Bare @verified usage
        return _verify_and_wrap(
            func, pre, post, raise_on_failure, timeout_ms, contracts, check_contracts
        )

    # @verified(...) usage — return a decorator
    def decorator(fn: F) -> F:
        return _verify_and_wrap(
            fn, pre, post, raise_on_failure, timeout_ms, contracts, check_contracts
        )

    return decorator  # type: ignore[return-value]