tlaw 0.0.2

Write and enforce executable behavioral laws for Python code.

tlaw

tlaw lets ordinary Python code state behavior that an implementation must continue to satisfy. The law file is executable and is the source of truth; Hypothesis generates and shrinks inputs underneath it.

For the exact implemented surface and its limits, see current tlaw behavior. Design documents are kept separate because they may describe syntax that does not exist yet.

Install

uv add --dev tlaw        # inside a project (recommended)
uv tool install tlaw     # or: the CLI on its own

The project install is recommended because laws are ordinary Python: when a law imports your project's own dependencies, tlaw must run in the same environment (uv run tlaw check laws.py). The standalone tool works for self-contained law folders whose implementation needs only the standard library.

What works today

tlaw currently has a small beginner interface plus explicit tools for narrower domains, structural comparison, stateful paths, and mutation evidence:

• @tlaw.law turns an ordinary annotated Python function into an executable law;
• simple annotations such as str, int, and list[int] supply generated inputs;
• number(...), integer(...), one_of(...), and list_of(...) define visible finite-float, bounded-integer, finite-choice, and list domains without Hypothesis syntax;
• depends(...) derives one parameter's domain from another's generated value, so relational inputs are generated correctly by construction;
• same(..., within=..., relative=...) compares nested values and array-like values with explicit absolute and relative tolerances and reports the first difference;
• raises(Expected, function, ...) states an exception contract whose failure names what actually happened instead of returning False;
• tlaw check laws.py --explain runs the laws and reports what it generated;
• inferred laws use deterministic runs and show Hypothesis's minimized failing input;
• a passing inferred law is rejected when tlaw detects that it mutated its generated input;
• system, call, then, and same_as cover explicit stateful paths; and
• tlaw mutate laws.py implementation.py challenges the laws with generated mutations of one module and shows every survivor, for a flat feature folder or a module inside an installed package.

Important pieces are still intentionally absent: domain predicates and nested domain positions beyond the implemented number, integer, list_of, one_of, depends, and supported Annotated forms; whole-folder checking; opt-in third-party pytest plugins; impact graphs; and commands for diffing, randomized search, or replay. Documentation that discusses those directions does not make them usable syntax.

Write a first law

Given an ordinary function:

# implementation.py
def reverse(values: list[int]) -> list[int]:
    return list(reversed(values))

Its law can be one function:

# laws.py
import tlaw

from implementation import reverse


@tlaw.law
def reversing_twice_returns_the_original(values: list[int]) -> bool:
    return reverse(reverse(values)) == values

Run it:

tlaw check laws.py

To see what tlaw inferred rather than taking generation on trust:

tlaw check laws.py --explain

The function name explains the behavior, its annotation supplies generated inputs, and the returned boolean is what must always hold. Writing this first law requires no Hypothesis syntax.

Bare laws run up to 100 deterministic examples without a local example database. tlaw includes the minimized failing input in its output. It also copies generated inputs and rejects a passing bare law when it detects that the law mutated one; stateful behavior should use the explicit path interface below.

State a narrower domain and comparison

When a plain type is broader than the application's real inputs, name the accepted values beside the laws:

import tlaw

from rewards import center


Reward = tlaw.number(0, 1)
Rewards = tlaw.list_of(Reward, min_size=1, max_size=20)


@tlaw.law
def centered_rewards_sum_to_zero(rewards: Rewards) -> tlaw.Comparison:
    return tlaw.same(sum(center(rewards)), 0.0, within=1e-12)

number(0, 1) means finite floats from 0 through 1, including both bounds. list_of makes the element and size domain visible in --explain. within=1e-12 means absolute tolerance at every numeric leaf; omitting it means exact comparison. For values whose magnitude is large or unknown, add relative=1e-9 — the two combine like math.isclose, and the rescale example shows why a numerical refactor needs it. same also compares nested lists, tuples, dictionaries, and array-like objects exposing shape, dtype, and tolist().

Domain aliases are runtime values, so strict type checkers may flag rewards: Rewards. The checker-clean spelling wraps the domain in Annotated — type Reward = Annotated[float, tlaw.number(0, 1)] used as rewards: list[Reward] — where the base type is for the checker and tlaw enforces the domain; see current tlaw behavior. Annotated metadata other than exactly one tlaw domain, and domains in positions tlaw cannot generate from yet, are rejected rather than silently ignored. tlaw does not yet verify that the base type and attached domain agree, so the author must keep them consistent.

The complete runnable version is in the rewards example.

For a larger first exercise, open the self-contained name cleaner tutorial. It explains every definition, includes implementation and laws together, and gives a deliberate break-and-fix exercise. The tiny list example and the current interface direction remain available as references.

Keep laws beside the code whose behavior they define. A feature folder should remain understandable on its own; tlaw does not require a distant contract registry or hidden configuration for a local law.

Git and CI are the acceptance mechanism

A law committed to the repository is accepted behavior. tlaw does not maintain a second approval database. Law changes are ordinary reviewable code changes, and the repository's CI should enforce the resulting source of truth:

tlaw check path/to/feature/laws.py --explain

This repository enforces itself with one visible gate, scripts/gate: the committed dependency lock, ruff, the full property suite, and tlaw check plus tlaw mutate on the flat examples — the repo dogfoods its own strength meter on every push. CI pins uv and runs the gate on every push and pull request (.github/workflows/ci.yml), and the same file runs locally before each push once the hook is installed:

git config core.hooksPath .githooks

Local and remote checks share one script instead of maintaining two command lists. CI also pins uv, and the gate refuses a stale dependency lock. git push --no-verify skips the local run in an emergency; CI remains the enforcement of record. Publishing stays separate: the release workflow is gatekept by a version change in pyproject.toml.

If a commit intentionally changes behavior, its executable law and implementation may change together. The law diff states what changed; CI checks that the implementation now obeys it on every push and pull request.

Probe a codebase without modifying it

Laws can be written against any installed project before that project adopts tlaw. Put a laws file in a scratch directory, import the project's real functions, and run tlaw inside the project's own environment:

uv run --project path/to/project --with tlaw tlaw check laws.py

--project supplies the target's dependencies; --with injects tlaw for the run only. Nothing in the target repository changes — no pyproject edit, no committed files — which makes this the cheapest honest way to answer "would laws hold on this code?" before adopting anything. The documented kvfit probe ran this way and paid for features with its findings.

Release to PyPI

Changing [project].version in pyproject.toml on main is the release signal. The workflow compares that value with the version before the push. An unchanged version never publishes; a changed version must pass the lockfile, compiled-changelog, lint, test, build, and distribution checks before it reaches PyPI.

During development, add one small file under changes/ for each user-visible change instead of editing CHANGELOG.md. The complete rules are in CONTRIBUTING.md. At release, use uv to keep the version and lockfile together, then compile and review those fragments:

uv version 0.0.3
uv run towncrier build --yes --version 0.0.3
git diff -- CHANGELOG.md changes pyproject.toml uv.lock
git add pyproject.toml uv.lock CHANGELOG.md changes/
git commit -m "chore(release): publish tlaw 0.0.3"
git push origin main

The upload uses PyPI trusted publishing, not a long-lived API token. Its one-time configuration must name GitHub owner teilomillet, repository tlaw, workflow release.yml, and environment pypi. The workflow is kept in .github/workflows/release.yml.

Describe stateful paths

When behavior mutates an object, a law can instead compare two paths from fresh starts:

from hypothesis import strategies as st

import tlaw
from wallet import Wallet


money = st.integers(min_value=0)
wallet = tlaw.system(
    Wallet,
    observe=lambda value: value.balance,
)


@tlaw.law(
    "deposit then withdraw changes nothing",
    balance=money,
    amount=money,
)
def deposit_round_trip(balance, amount):
    start = wallet(balance)
    return (
        start
        .call("deposit", amount)
        .call("withdraw", amount)
        .same_as(start)
    )

Run it in the same way:

tlaw check laws.py

The stateful path interface adds four ideas:

• system(...) defines how to construct fresh values and what to observe;
• @law(...) supplies ordinary Hypothesis strategies;
• .call(...) or .then(...) extends a path; and
• .same_as(...) says two paths must agree.

Law functions do not need pytest's test_ prefix. They are still executable Hypothesis tests and can also be run directly with pytest.

See the complete mutable wallet laws and the smaller pure UTF-8 round-trip law.

Why paths

tlaw models each program as an immutable sequence of steps. Composition is sequence concatenation, and the identity is the empty sequence. This gives the categorical rules—associativity and left/right identity—structurally, before application-specific testing begins.

A domain law is then an equation between two executable paths:

                 deposit(amount)     withdraw(amount)
wallet(balance) ──────────────────────────────────────► result
       │
       └──────────────── do nothing ──────────────────► expected

                         result == expected

For mutable application code, each path constructs its own fresh objects. For pure code, .then(function) uses the function's return value as the next value.

Check versus audit

Human-authored laws and audit evidence are deliberately separate:

tlaw check laws.py
tlaw audit audit.py

• check runs the laws against the current implementation.
• audit runs those same laws against a passing baseline and declared known-wrong implementations.

The wallet's audit declaration is separate from its laws, so someone writing a law does not need to think about mutation testing or audit plumbing.

Run the intentionally weak audit:

uv run tlaw audit examples/wallet/tlaw-weak.toml

It excludes the zero-transfer law and exposes the gap:

Strength: 3/4 (75.0%)
Verdict: INSUFFICIENT

Run the complete declared audit:

uv run tlaw audit examples/wallet/audit.py

Strength: 4/4 (100.0%)
Verdict: SUFFICIENT FOR DECLARED KNOWN-WRONG SET

That verdict is deliberately narrow. It does not prove that the wallet is universally correct. It establishes that the baseline passes and every declared known-wrong implementation is rejected by a law.

Challenge laws with generated mutations

The audit's known-wrong set is chosen by its author. tlaw mutate generates challenges nobody selected — small single-site changes to one implementation module — and runs the unchanged laws against every one:

tlaw mutate laws.py implementation.py

Canary: KILLED (laws observe the mutated module)
Mutations:
- 3e67f984ab5f SURVIVED double_all: replace value + value with value - value
- f3bb33e45d2b KILLED sign: replace value < 0 with value <= 0 (law: laws.py::sign_matches_a_reference)
Killed 3 of 4 runnable generated mutations.
Survivors: 1

The rules are recorded in generated mutation evidence and encoded in tlaw/mutation.py: the baseline must pass first; an exception or a calibrated timeout under a mutant is a kill; a load failure is invalid, never a kill; a kill that does not replay is an error; and every survivor stays visible — the statement is never compressed into a percentage.

The canary runs by default before anything is scored: a poisoned copy of the implementation, in which every function raises, must be rejected by the laws. If it survives, the laws never observed the boundary module — typically because they import an installed package instead of the sibling file — and the report says INVALID EVIDENCE instead of listing meaningless survivors. There is no opt-out; the canary protects exactly the user who has never heard of it.

A survivor a human has investigated can be recorded in a committed TOML ledger and passed with --equivalents equivalents.toml; entries contradicted by evidence are reported as stale instead of being silently honored. Mutation IDs are content-based, so they survive edits elsewhere in the module.

Start a new feature law-first

For new code, the recommended shape makes mutation evidence free from day one:

feature/
├── implementation.py
└── laws.py            # imports: from implementation import ...

Write the laws first and watch them fail; implement until tlaw check passes; then run tlaw mutate to measure whether the laws actually constrain the implementation. Because the folder is flat and the laws import the module by name, the mutation boundary is wired by construction — the canary confirms it on every run.

Two worked examples record real runs end to end: examples/score_weights includes a genuine surviving mutant explained in a committed equivalence ledger, and examples/batch_packer is a full law-first development session — seven laws red before any implementation existed, then 13 of 13 mutants killed — with its findings in the law-first experiment record.

Use it from Python

import tlaw

check = tlaw.check("laws.py")
if not check.passed:
    print(check.output)

report = tlaw.audit("audit.py")
print(report)
report.enforce()

mutations = tlaw.mutate("laws.py", "implementation.py")
print(mutations)

report.enforce() raises tlaw.EnforcementError when evidence is invalid or insufficient. Its error.result retains the structured audit evidence.

Existing TOML audit manifests remain supported. Python law and audit files are executable code, so run only files you trust.

Develop tlaw

tlaw is itself developed property-first:

uv run pytest -q
uv run ruff check .
uv run ruff format --check .

The precise implemented surface is recorded in current tlaw behavior, and the independent challenge rules are recorded in generated mutation evidence.