Efct

简体中文

Efct is a static effect and pure-function verifier for a closed, auditable subset of Python. It checks what a function can observe, change, raise, or fail to return from, and rejects code it cannot prove safe.

Efct is currently alpha software. It supports CPython 3.13 and 3.14.

Installation

Install Efct from PyPI:

python -m pip install efct

With uv:

uv add efct

Confirm the installation:

efct --version

Quick start

Decorate a function with @efct.pure:

import efct


@efct.pure
def add(left: int, right: int) -> int:
    return left + right


assert add(2, 3) == 5

When the module is imported, Efct validates its source, types, calls, and effects. A successful decoration returns a verified PureFunction. Validation failure raises EfctStartupError and stops the module from importing.

You can also check files without importing them:

efct check app.py
efct check src/

Efct rejects unknown syntax, unknown calls, mutable values crossing function boundaries, and behavior outside a declared effect bound. It never treats unverified code as pure.

Pure functions and partial behavior

Efct separates external effects from partial behavior:

• External effects interact with or depend on the outside world, such as files, networks, clocks, randomness, environment variables, processes, and global state.
• Partial behavior means a computation may not return normally, such as raising an exception or diverging.

The three forms of pure have deliberately different meanings:

Use the bare decorator while implementing a function:

@efct.pure
def parse(value: str) -> int:
    if value == "":
        raise ValueError("empty")
    return 1

Efct infers Raise(ValueError) and propagates it to callers.

Use an explicit allowlist at a stable API boundary:

@efct.pure(efct.partial.Raise(ValueError))
def parse(value: str) -> int:
    if value == "":
        raise ValueError("empty")
    return 1

Use empty parentheses when the function must have no modeled partial behavior and must be proven to terminate:

@efct.pure()
def increment(value: int) -> int:
    return value + 1

Efct models these partial behaviors:

• efct.partial.Raise(ExceptionType)
• efct.partial.RaiseGroup(ExceptionType)
• efct.partial.Diverge()

An explicit declaration is an upper bound. A function may produce fewer behaviors than declared, but it cannot produce an undeclared one.

Declaring effects

Use @efct.effects(...) when a function intentionally interacts with the outside world:

import efct


@efct.effects(
    efct.effect.Console(),
    efct.partial.Raise(OSError),
    efct.partial.Raise(ValueError),
)
def show(value: int) -> None:
    print(value)

print has a console effect and may fail with the modeled OSError or ValueError paths. All three behaviors are therefore part of the public bound.

Available external effect declarations are:

• efct.effect.Console()
• efct.effect.File.Read() and efct.effect.File.Write()
• efct.effect.Network()
• efct.effect.Clock()
• efct.effect.Random()
• efct.effect.Environment()
• efct.effect.Process()
• efct.effect.State.Read() and efct.effect.State.Write()
• efct.effect.Unsafe()

Stable string declarations remain available:

@efct.effects("console", "raise:builtins.OSError", "raise:builtins.ValueError")
def show(value: int) -> None:
    print(value)

Do not mix typed declarations and string declarations in the same decorator.

Handling exceptions

Handled exceptions are removed from the outward partial bound:

@efct.pure()
def item_or_zero(values: tuple[int, ...], index: int) -> int:
    try:
        return values[index]
    except IndexError:
        return 0

Efct tracks exception inheritance, ordered handlers, except ... as error, exact re-raising, try ... else, finally, contextlib.suppress, exception groups, and supported except* flows. Unmatched exceptions continue to propagate.

For expected application failures, prefer Result data:

@efct.pure
def parse(value: str) -> efct.Result[int, str]:
    if value == "":
        return efct.Err("empty")
    return efct.Ok(1)

Result supports exhaustive match over Ok and Err.

Pure records

The same decorator can verify a deeply immutable record:

from dataclasses import dataclass

import efct


@efct.pure
@dataclass(frozen=True, slots=True)
class Point:
    x: int
    y: int

Values crossing a verified function boundary must belong to Efct's supported immutable value model.

Higher-order functions

PureCallable accepts a verified function with an explicitly empty effect and partial bound:

@efct.pure()
def apply(
    function: efct.PureCallable[[int], int],
    value: int,
) -> int:
    return function(value)

Effect-polymorphic functions preserve the concrete effects of a callback:

@efct.effects
def apply_effect[E: efct.EffectSet](
    function: efct.EffectCallable[[int], int, E],
    value: int,
) -> int:
    return function(value)

The effect variable E is instantiated from the callback certificate at each call site.

Module initialization

Function decorators do not automatically certify arbitrary top-level module code. Declare a module initialization contract with the reserved _efct name:

import efct

_efct = efct.pure

For effectful initialization, declare an explicit upper bound:

_efct = efct.effects(
    efct.effect.Console(),
    efct.partial.Raise(OSError),
    efct.partial.Raise(ValueError),
)

Without _efct, the module may still run, but Efct makes no claim about its initialization effects.

Command line

efct check app.py
efct check src/
efct check src/ --format=json
efct check src/ --verified-only
efct check src/ --deny-unsafe
efct trust fingerprint pytest
efct run app.py
efct --version

efct check analyzes code without executing it. A zero exit status means the source snapshot described by the report passed verification.

efct run verifies the entry point and its local dependency closure before executing a verified source snapshot. Change the source, dependencies, or Python runtime and it must be checked again.

External libraries

Third-party symbols are never considered pure automatically. Declare an unaudited boundary explicitly when migration is still in progress:

schema = 1

[[symbol]]
trust = "unsafe"
path = "legacy.math.clamp"
signature = "(int, int, int) -> int"
effects = []
partials = []
reason = "the implementation has not been audited"

An unsafe call contributes the unsafe effect. Use --deny-unsafe in CI to reject it.

An audited boundary binds the public contract to exact installed distributions and to the callable's real implementation:

schema = 1

[python]
implementation = "cpython"
version = "3.14.7"
cache_tag = "cpython-314"

[[distribution]]
name = "ourlib"
version = "1.4.2"
installation_sha256 = "..."
dependencies = []

[[symbol]]
trust = "audited"
path = "ourlib.math.clamp"
owner = "ourlib"
implementation = { kind = "python", path = "ourlib.math.clamp" }
signature = "(int, int, int) -> int"
effects = []
partials = []

Generate the installation fields instead of calculating the digest manually:

efct trust fingerprint ourlib
efct trust fingerprint ourlib --format=json

List every audited direct dependency in dependencies and add a corresponding [[distribution]] block. Native extension functions use kind = "native". Efct rejects stale digests, missing installation records, editable installations, undeclared dependency references, mismatched module ownership, replaced runtime callables, and Python code objects that do not match the hashed installation source. It never falls back from audited to unsafe.

path is the public export used by application code. implementation.path identifies the function that actually implements it, so audited re-exports can point into a declared dependency. effects contains only external effects; partials contains raise:..., raise-group:..., or diverge.

Runtime enforcement

Verified wrappers enforce the certificate when called:

• EfctContractError reports an argument contract violation.
• EfctIntegrityError reports changed code, bindings, dependencies, or an invalid return value.
• EfctStartupError reports source or verification failure during decoration.

Argument and return types are exact. Rebinding a verified dependency invalidates the certificate instead of silently widening it. Audited distribution contents are checked when the certificate is issued; subsequent calls revalidate the loaded object identities and Python code object identity.

Supported Python boundary

Efct intentionally supports a strict subset of Python. Common supported features include immutable primitive values, tuples, frozenset, FrozenMap, optional values, Result, local control flow, finite iteration, analyzed while loops, restricted local lists, static imports, verified cross-module calls, and registered standard-library operations.

Dynamic imports, reflection, monkey patching, ordinary mutable objects crossing boundaries, unknown third-party calls, and unsupported context managers are rejected. Efct is a verifier, not a Python sandbox.

License

Efct is available under the MIT License.