provably.engine¶

Proof certificates, Z3 orchestration, and cache management.

from provably.engine import ProofCertificate, Status, verify_function, verify_module, clear_cache, configure

`Status`¶

Value	Meaning
`VERIFIED`	Z3 returned `unsat`. Mathematical theorem.
`COUNTEREXAMPLE`	Z3 returned `sat`. Counterexample found.
`UNKNOWN`	Solver timed out.
`TRANSLATION_ERROR`	AST translator failed.
`SKIPPED`	Not attempted (no Z3, async, no postcondition).

`ProofCertificate`¶

Immutable certificate attached to every @verified function as fn.__proof__.

cert = fn.__proof__
cert.verified        # True iff status == VERIFIED
cert.status          # Status.VERIFIED
cert.counterexample  # {'x': 3, '__return__': 1} or None
cert.solver_time_ms  # 1.4
cert.message         # human-readable summary
str(cert)            # "[Q.E.D.] fn_name"

Field	Type	Description
`function_name`	`str`	Verified function name
`source_hash`	`str`	SHA-256 prefix (content-addressing)
`status`	`Status`	Verification outcome
`preconditions`	`tuple[str, ...]`	Z3 precondition strings
`postconditions`	`tuple[str, ...]`	Z3 postcondition strings
`counterexample`	`dict \\| None`	Witness on `COUNTEREXAMPLE`
`message`	`str`	Error/skip/counterexample summary
`solver_time_ms`	`float`	Wall-clock ms in Z3
`z3_version`	`str`	Z3 version used

Serialization¶

data = cert.to_json()                    # dict (JSON-serializable)
cert = ProofCertificate.from_json(data)  # round-trip

`verify_function()`¶

Low-level entry point. Most users should use @verified instead.

from provably.engine import verify_function

def add(x: int, y: int) -> int:
    return x + y

cert = verify_function(add, pre=lambda x, y: x >= 0, post=lambda x, y, result: result >= x)
cert.verified  # True

`verify_module()`¶

Collect all @verified functions in a module, return {name: ProofCertificate}.

from provably.engine import verify_module
import mypackage.math as m

results = verify_module(m)
for name, cert in results.items():
    print(cert)  # [Q.E.D.] name

`configure()`¶

Set global defaults. Call before importing decorated modules.

Key	Default	Description
`timeout_ms`	`5000`	Z3 timeout per proof (ms)
`raise_on_failure`	`False`	Raise `VerificationError` on failure
`log_level`	`"WARNING"`	Logging level for `provably` logger

from provably import configure
configure(timeout_ms=10_000, raise_on_failure=True)

`clear_cache()`¶

Clear the global proof cache (content-addressed by source + contract hash).

from provably.engine import clear_cache
clear_cache()

provably.engine ¶

Verification engine — VC generation, Z3 solving, proof certificates.

Orchestrates the full pipeline

Parse function source → AST
Create Z3 symbolic variables from type annotations
Translate function body via Translator (the TCB)
Build verification condition: pre ∧ body → post
Negate postcondition, check UNSAT with Z3
Return ProofCertificate (cached, content-addressed)

Global configuration¶

Use :func:configure to set defaults that apply to every subsequent call::

from provably import configure
configure(timeout_ms=10_000, raise_on_failure=True)

These defaults can be overridden per-call via keyword arguments to :func:verify_function or the :func:~provably.decorators.verified decorator.

Classes¶

ProofCertificate `dataclass` ¶

ProofCertificate(function_name: str, source_hash: str, status: Status, preconditions: tuple[str, ...], postconditions: tuple[str, ...], counterexample: dict[str, Any] | None = None, message: str = '', solver_time_ms: float = 0.0, z3_version: str = '')

Immutable proof certificate for a verified function.

Attached to decorated functions as func.__proof__.

Attributes:

Name	Type	Description
`function_name`	`str`	The name of the verified function.
`source_hash`	`str`	SHA-256 prefix of the function's source text.
`status`	`Status`	The verification outcome (see :class:`Status`).
`preconditions`	`tuple[str, ...]`	Human-readable Z3 string representations of the applied preconditions.
`postconditions`	`tuple[str, ...]`	Human-readable Z3 string representations of the applied postconditions.
`counterexample`	`dict[str, Any] \| None`	Input values that disprove the postcondition, or `None` if not applicable.
`message`	`str`	Human-readable explanation (error message, skip reason, etc.).
`solver_time_ms`	`float`	Wall-clock time spent in the Z3 solver.
`z3_version`	`str`	The Z3 version string used for this proof.

Attributes¶

verified `property` ¶

verified: bool

True iff the status is :attr:Status.VERIFIED.

Functions¶

explain ¶

explain() -> str

Human-readable explanation of the proof result.

Returns a multi-line string describing the outcome, any counterexample found, and the violated postcondition.

Example::

print(func.__proof__.explain())
# Q.E.D.: double
# or
# COUNTEREXAMPLE: bad_func
#   Counterexample: {'x': -1}
#   bad_func(x=-1) = -1
#   Postcondition: 0 <= result

Source code in src/provably/engine.py

def explain(self) -> str:
    """Human-readable explanation of the proof result.

    Returns a multi-line string describing the outcome, any counterexample
    found, and the violated postcondition.

    Example::

        print(func.__proof__.explain())
        # Q.E.D.: double
        # or
        # COUNTEREXAMPLE: bad_func
        #   Counterexample: {'x': -1}
        #   bad_func(x=-1) = -1
        #   Postcondition: 0 <= result
    """
    lines = [
        f"{'Q.E.D.' if self.verified else self.status.value.upper()}: {self.function_name}"
    ]
    if self.counterexample:
        args = {k: v for k, v in self.counterexample.items() if k != "__return__"}
        ret = self.counterexample.get("__return__")
        lines.append(f"  Counterexample: {args}")
        if ret is not None:
            lines.append(
                f"  {self.function_name}({', '.join(f'{k}={v}' for k, v in args.items())}) = {ret}"
            )
        for post in self.postconditions:
            lines.append(f"  Postcondition: {post}")
    if self.message:
        lines.append(f"  {self.message}")
    return "\n".join(lines)

from_json `classmethod` ¶

from_json(data: dict[str, Any]) -> ProofCertificate

Deserialize a certificate from a JSON-compatible dict.

This is the inverse of :meth:to_json.

Parameters:

Name	Type	Description	Default
`data`	`dict[str, Any]`	A dict with the same keys as produced by :meth:`to_json`.	required

Returns:

Type	Description
`ProofCertificate`	A reconstructed :class:`ProofCertificate`.

Raises:

Type	Description
`KeyError`	If a required field is missing from data.
`ValueError`	If the `status` value is not a valid :class:`Status`.

Example::

cert = ProofCertificate.from_json(json.loads(json_string))

Source code in src/provably/engine.py

@classmethod
def from_json(cls, data: dict[str, Any]) -> ProofCertificate:
    """Deserialize a certificate from a JSON-compatible dict.

    This is the inverse of :meth:`to_json`.

    Args:
        data: A dict with the same keys as produced by :meth:`to_json`.

    Returns:
        A reconstructed :class:`ProofCertificate`.

    Raises:
        KeyError: If a required field is missing from *data*.
        ValueError: If the ``status`` value is not a valid :class:`Status`.

    Example::

        cert = ProofCertificate.from_json(json.loads(json_string))
    """
    return cls(
        function_name=data["function_name"],
        source_hash=data["source_hash"],
        status=Status(data["status"]),
        preconditions=tuple(data.get("preconditions", [])),
        postconditions=tuple(data.get("postconditions", [])),
        counterexample=data.get("counterexample"),
        message=data.get("message", ""),
        solver_time_ms=float(data.get("solver_time_ms", 0.0)),
        z3_version=data.get("z3_version", ""),
    )

to_json ¶

to_json() -> dict[str, Any]

Serialize the certificate to a JSON-compatible dict.

All values are JSON-native types (str, int, float, bool, None, dict). The counterexample values are coerced to strings when they are not already JSON-serializable.

Returns:

Type	Description
`dict[str, Any]`	A dict that can be passed directly to `json.dumps()`.

Example::

import json
cert = func.__proof__
print(json.dumps(cert.to_json(), indent=2))

Source code in src/provably/engine.py

def to_json(self) -> dict[str, Any]:
    """Serialize the certificate to a JSON-compatible dict.

    All values are JSON-native types (str, int, float, bool, None, dict).
    The ``counterexample`` values are coerced to strings when they are
    not already JSON-serializable.

    Returns:
        A dict that can be passed directly to ``json.dumps()``.

    Example::

        import json
        cert = func.__proof__
        print(json.dumps(cert.to_json(), indent=2))
    """
    ce: dict[str, Any] | None = None
    if self.counterexample is not None:
        ce = {}
        for k, v in self.counterexample.items():
            if isinstance(v, int | float | bool | str | type(None)):
                ce[k] = v
            else:
                ce[k] = str(v)
    return {
        "function_name": self.function_name,
        "source_hash": self.source_hash,
        "status": self.status.value,
        "preconditions": list(self.preconditions),
        "postconditions": list(self.postconditions),
        "counterexample": ce,
        "message": self.message,
        "solver_time_ms": self.solver_time_ms,
        "z3_version": self.z3_version,
    }

to_prompt ¶

to_prompt() -> str

Format certificate for LLM consumption in repair loops.

Returns a single-paragraph string describing the verification result in a form suitable for inclusion in an LLM prompt.

Example::

prompt = func.__proof__.to_prompt()
# "Function `bad_func` DISPROVED. Counterexample: {'x': -1} → result=-1
#  Violated: 0 <= result Fix the implementation or strengthen the precondition."

Source code in src/provably/engine.py

def to_prompt(self) -> str:
    """Format certificate for LLM consumption in repair loops.

    Returns a single-paragraph string describing the verification result
    in a form suitable for inclusion in an LLM prompt.

    Example::

        prompt = func.__proof__.to_prompt()
        # "Function `bad_func` DISPROVED. Counterexample: {'x': -1} → result=-1
        #  Violated: 0 <= result Fix the implementation or strengthen the precondition."
    """
    if self.verified:
        return (
            f"Function `{self.function_name}` VERIFIED. "
            "All inputs satisfying preconditions produce valid outputs."
        )
    if self.status == Status.COUNTEREXAMPLE:
        args = {k: v for k, v in self.counterexample.items() if k != "__return__"}  # type: ignore[union-attr]
        ret = self.counterexample.get("__return__")  # type: ignore[union-attr]
        parts = [f"Function `{self.function_name}` DISPROVED."]
        parts.append(f"Counterexample: {args} → result={ret}")
        if self.postconditions:
            parts.append(f"Violated: {self.postconditions[0]}")
        parts.append("Fix the implementation or strengthen the precondition.")
        return " ".join(parts)
    return f"Function `{self.function_name}`: {self.status.value}. {self.message}"

Status ¶

Bases: Enum

Verification result status.

Functions¶

clear_cache ¶

clear_cache() -> None

Clear the in-memory proof cache.

Does not delete disk-cached proofs. To clear disk cache, delete the directory set via configure(cache_dir=...).

Source code in src/provably/engine.py

def clear_cache() -> None:
    """Clear the in-memory proof cache.

    Does **not** delete disk-cached proofs. To clear disk cache, delete
    the directory set via ``configure(cache_dir=...)``.
    """
    _proof_cache.clear()

configure ¶

configure(**kwargs: Any) -> None

Set global verification defaults.

Supported keys:

timeout_ms (int): Z3 solver timeout in milliseconds (default 5000).
raise_on_failure (bool): Raise :class:~provably.decorators.VerificationError when a proof fails (default False).
log_level (str): Python logging level for the provably logger (default "WARNING").
cache_dir (str | None): Directory for disk-persistent proof cache. Default: ~/.provably/cache. Set to None to disable disk caching. Proofs are persisted across process restarts — no re-proving on import.

Example::

from provably import configure
configure(timeout_ms=10_000, cache_dir=".provably_cache")

Parameters:

Name	Type	Description	Default
`**kwargs`	`Any`	Key-value pairs to update in the global config.	`{}`

Raises:

Type	Description
`ValueError`	If an unknown configuration key is provided.

Source code in src/provably/engine.py

def configure(**kwargs: Any) -> None:
    """Set global verification defaults.

    Supported keys:

    - ``timeout_ms`` (int): Z3 solver timeout in milliseconds (default 5000).
    - ``raise_on_failure`` (bool): Raise :class:`~provably.decorators.VerificationError`
      when a proof fails (default ``False``).
    - ``log_level`` (str): Python logging level for the ``provably`` logger
      (default ``"WARNING"``).
    - ``cache_dir`` (str | None): Directory for disk-persistent proof cache.
      Default: ``~/.provably/cache``. Set to ``None`` to disable disk caching.
      Proofs are persisted across process restarts — no re-proving on import.

    Example::

        from provably import configure
        configure(timeout_ms=10_000, cache_dir=".provably_cache")

    Args:
        **kwargs: Key-value pairs to update in the global config.

    Raises:
        ValueError: If an unknown configuration key is provided.
    """
    unknown = set(kwargs) - set(_config)
    if unknown:
        raise ValueError(f"Unknown configure() keys: {sorted(unknown)}")
    _config.update(kwargs)

    if "log_level" in kwargs:
        import logging

        logging.getLogger("provably").setLevel(
            getattr(logging, kwargs["log_level"], logging.WARNING)
        )

verify_function ¶

verify_function(func: Callable[..., Any], pre: Callable[..., Any] | None = None, post: Callable[..., Any] | None = None, timeout_ms: int | None = None, verified_contracts: dict[str, dict[str, Any]] | None = None) -> ProofCertificate

Verify a Python function using Z3.

Parameters:

Name	Type	Description	Default
`func`	`Callable[..., Any]`	The function to verify.	required
`pre`	`Callable[..., Any] \| None`	Precondition lambda taking the same args as func. Use `&` instead of `and`, `\|` instead of `or`.	`None`
`post`	`Callable[..., Any] \| None`	Postcondition lambda taking `(*args, result)`.	`None`
`timeout_ms`	`int \| None`	Z3 solver timeout in milliseconds. Defaults to the global `timeout_ms` set via :func:`configure` (5000ms).	`None`
`verified_contracts`	`dict[str, dict[str, Any]] \| None`	Contracts of called functions for composition.	`None`

Returns:

Type	Description
`ProofCertificate`	class:`ProofCertificate` with status `VERIFIED`, `COUNTEREXAMPLE`,
`ProofCertificate`	`UNKNOWN`, `TRANSLATION_ERROR`, or `SKIPPED`.

Source code in src/provably/engine.py

def verify_function(
    func: Callable[..., Any],
    pre: Callable[..., Any] | None = None,
    post: Callable[..., Any] | None = None,
    timeout_ms: int | None = None,
    verified_contracts: dict[str, dict[str, Any]] | None = None,
) -> ProofCertificate:
    """Verify a Python function using Z3.

    Args:
        func: The function to verify.
        pre: Precondition lambda taking the same args as *func*.
             Use ``&`` instead of ``and``, ``|`` instead of ``or``.
        post: Postcondition lambda taking ``(*args, result)``.
        timeout_ms: Z3 solver timeout in milliseconds.  Defaults to
            the global ``timeout_ms`` set via :func:`configure` (5000ms).
        verified_contracts: Contracts of called functions for composition.

    Returns:
        :class:`ProofCertificate` with status ``VERIFIED``, ``COUNTEREXAMPLE``,
        ``UNKNOWN``, ``TRANSLATION_ERROR``, or ``SKIPPED``.
    """
    if timeout_ms is None:
        timeout_ms = int(_config["timeout_ms"])

    fname = getattr(func, "__name__", str(func))

    # Get source
    try:
        source = textwrap.dedent(inspect.getsource(func))
    except (OSError, TypeError) as e:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.SKIPPED,
            preconditions=(),
            postconditions=(),
            message=f"Cannot get source: {e}",
        )

    # Cache key: source + contract bytecode (stable across identical lambdas)
    cache_key = _source_hash(source + _contract_sig(pre) + _contract_sig(post))
    if cache_key in _proof_cache:
        return _proof_cache[cache_key]
    disk_hit = _load_from_disk(cache_key)
    if disk_hit is not None:
        return disk_hit

    # Parse AST
    tree = ast.parse(source)
    func_ast = tree.body[0]
    if not isinstance(func_ast, ast.FunctionDef):
        return _err(fname, source, "Expected a function definition")

    # Resolve type hints
    try:
        hints = get_type_hints(func, include_extras=True)
    except Exception:
        hints = {}

    # Create Z3 symbolic variables for parameters
    param_vars: dict[str, Any] = {}
    param_types: dict[str, type] = {}
    for arg in func_ast.args.args:
        name = arg.arg
        typ = hints.get(name, float)
        param_types[name] = typ
        param_vars[name] = make_z3_var(name, typ)

    # Validate contract arities
    n_params = len(param_vars)
    if pre is not None:
        err = _validate_contract_arity(pre, n_params, "pre", fname)
        if err:
            cert = _err(fname, source, err)
            _proof_cache[cache_key] = cert
            return cert

    if post is not None:
        err = _validate_contract_arity(post, n_params + 1, "post", fname)
        if err:
            cert = _err(fname, source, err)
            _proof_cache[cache_key] = cert
            return cert

    # Resolve module-level constants from func's global scope
    closure_vars = _resolve_closure_vars(func, tree, set(param_vars))

    # Translate function body
    translator = Translator(param_types, verified_contracts, closure_vars)
    try:
        result = translator.translate(func_ast, param_vars)
    except TranslationError as e:
        # Enrich with line-number context if not already present
        msg = str(e)
        try:
            # Walk AST to find a plausible line number
            first_line = next(
                (getattr(n, "lineno", None) for n in ast.walk(func_ast) if hasattr(n, "lineno")),
                None,
            )
            if first_line and "line" not in msg:
                msg = f"{msg} (in '{fname}', near line {first_line})"
        except Exception:
            pass
        cert = _err(fname, source, msg)
        _proof_cache[cache_key] = cert
        return cert

    if result.return_expr is None:
        cert = _err(fname, source, "Function has no return value on all paths")
        _proof_cache[cache_key] = cert
        return cert

    # Build solver
    s = z3.Solver()
    s.set("timeout", timeout_ms)

    # 1. Add preconditions
    pre_strs: list[str] = []
    param_list = [param_vars[arg.arg] for arg in func_ast.args.args]

    if pre is not None:
        try:
            pre_z3 = pre(*param_list)
            if isinstance(pre_z3, z3.BoolRef):
                s.add(pre_z3)
                pre_strs.append(str(pre_z3))
            else:
                cert = _err(
                    fname,
                    source,
                    f"Precondition returned {type(pre_z3).__name__}, expected z3.BoolRef. "
                    "Use & instead of 'and', | instead of 'or'.",
                )
                _proof_cache[cache_key] = cert
                return cert
        except Exception as e:
            cert = _err(
                fname,
                source,
                f"Precondition error: {e}. Use & instead of 'and', | instead of 'or'.",
            )
            _proof_cache[cache_key] = cert
            return cert

    # 2. Add refinement type constraints from annotations
    for name, var in param_vars.items():
        typ = hints.get(name)
        if typ is not None:
            for constraint in extract_refinements(typ, var):
                s.add(constraint)
                pre_strs.append(str(constraint))

    # 3. Add body constraints (assumptions: callee postconditions, asserts)
    for c in result.constraints:
        s.add(c)

    # 3b. Collect proof obligations (callee preconditions that caller must prove)
    # These go into the postcondition — they must hold, not just be assumed.
    caller_obligations: list[Any] = list(result.obligations)

    # 4. Build the combined postcondition
    post_parts: list[Any] = []
    post_strs: list[str] = []
    ret = result.return_expr

    if post is not None:
        try:
            post_z3 = post(*param_list, ret)
            if isinstance(post_z3, z3.BoolRef):
                post_parts.append(post_z3)
                post_strs.append(str(post_z3))
            else:
                cert = _err(
                    fname,
                    source,
                    f"Postcondition returned {type(post_z3).__name__}, expected z3.BoolRef.",
                )
                _proof_cache[cache_key] = cert
                return cert
        except Exception as e:
            cert = _err(fname, source, f"Postcondition error: {e}")
            _proof_cache[cache_key] = cert
            return cert

    # Return type refinements
    ret_typ = hints.get("return")
    if ret_typ is not None:
        for constraint in extract_refinements(ret_typ, ret):
            post_parts.append(constraint)
            post_strs.append(str(constraint))

    # Add caller obligations (callee preconditions) to postcondition set
    for ob in caller_obligations:
        post_parts.append(ob)
        post_strs.append(f"obligation: {ob}")

    # Nothing to prove
    if not post_parts:
        cert = ProofCertificate(
            function_name=fname,
            source_hash=_source_hash(source),
            status=Status.SKIPPED,
            preconditions=tuple(pre_strs),
            postconditions=(),
            message="No postcondition — nothing to prove",
        )
        _proof_cache[cache_key] = cert
        return cert

    # 5. Negate the combined postcondition
    combined_post = z3.And(*post_parts) if len(post_parts) > 1 else post_parts[0]
    s.add(z3.Not(combined_post))

    # 6. Solve
    t0 = time.monotonic()
    check = s.check()
    elapsed = (time.monotonic() - t0) * 1000

    z3_ver = z3.get_version_string()

    if check == z3.unsat:
        cert = ProofCertificate(
            function_name=fname,
            source_hash=_source_hash(source),
            status=Status.VERIFIED,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            z3_version=z3_ver,
        )
    elif check == z3.sat:
        ce = _extract_counterexample(s.model(), param_vars, ret)
        cert = ProofCertificate(
            function_name=fname,
            source_hash=_source_hash(source),
            status=Status.COUNTEREXAMPLE,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            counterexample=ce,
            message=f"Counterexample: {ce}",
            solver_time_ms=elapsed,
            z3_version=z3_ver,
        )
    else:
        cert = ProofCertificate(
            function_name=fname,
            source_hash=_source_hash(source),
            status=Status.UNKNOWN,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            message=f"Z3 returned unknown (timeout {timeout_ms}ms?)",
            z3_version=z3_ver,
        )

    _proof_cache[cache_key] = cert
    _save_to_disk(cache_key, cert)
    return cert

verify_module ¶

verify_module(module: ModuleType) -> dict[str, ProofCertificate]

Find all @verified functions in a module and return their certificates.

Walks the module's namespace looking for callables that have a __proof__ attribute (i.e. functions decorated with :func:~provably.decorators.verified).

Parameters:

Name	Type	Description	Default
`module`	`ModuleType`	A Python module object (e.g. from `import mymodule`).	required

Returns:

Type	Description
`dict[str, ProofCertificate]`	A dict mapping `function_name` to its :class:`ProofCertificate`.
`dict[str, ProofCertificate]`	Functions without a `__proof__` attribute are silently skipped.

Example::

import mymodule
from provably import verify_module

results = verify_module(mymodule)
for name, cert in results.items():
    print(cert)

Source code in src/provably/engine.py

def verify_module(module: _types.ModuleType) -> dict[str, ProofCertificate]:
    """Find all ``@verified`` functions in a module and return their certificates.

    Walks the module's namespace looking for callables that have a
    ``__proof__`` attribute (i.e. functions decorated with
    :func:`~provably.decorators.verified`).

    Args:
        module: A Python module object (e.g. from ``import mymodule``).

    Returns:
        A dict mapping ``function_name`` to its :class:`ProofCertificate`.
        Functions without a ``__proof__`` attribute are silently skipped.

    Example::

        import mymodule
        from provably import verify_module

        results = verify_module(mymodule)
        for name, cert in results.items():
            print(cert)
    """
    results: dict[str, ProofCertificate] = {}
    for attr_name in dir(module):
        try:
            obj = getattr(module, attr_name)
        except Exception:
            continue
        if callable(obj) and hasattr(obj, "__proof__"):
            cert: ProofCertificate = obj.__proof__
            results[cert.function_name] = cert
    return results

provably.engine¶

Status¶

ProofCertificate¶

Serialization¶

verify_function()¶

verify_module()¶

configure()¶

clear_cache()¶

provably.engine ¶

Global configuration¶

Classes¶

ProofCertificate dataclass ¶

Attributes¶

verified property ¶

Functions¶

explain ¶

from_json classmethod ¶

to_json ¶

to_prompt ¶

Status ¶

Functions¶

clear_cache ¶

configure ¶

verify_function ¶

verify_module ¶

`Status`¶

`ProofCertificate`¶

`verify_function()`¶

`verify_module()`¶

`configure()`¶

`clear_cache()`¶

ProofCertificate `dataclass` ¶

verified `property` ¶

from_json `classmethod` ¶