env

A trusted clauz3 layer for reading environment variables with name-based allowlists, blocklists, prefix vetoes, and a read-count bound — the canonical guard for any program that handles credentials via os.environ.

Unlike the layers under examples/, this effect is real, not a mock: read_env actually calls os.environ.get. The prover never runs the body — it records each call as a fact and proves the contract. The body runs only under clauz3 run, after a program is proved and approved.

Install

clauz3 install stdlib:env

Effects

Import with from tools.env.trusted.effects import read_env:

• read_env(name: str) -> str — return env var name, or the empty string if unset. Precondition: name is non-empty. Recorded under the read and env markers.

Contracts

Import with from tools.env.trusted import contracts as envc:

• envc.no_guarantees() — explicit null contract.
• envc.no_env_reads() — the program reads no env vars.
• envc.only_vars(allowlist) — every var name read is in allowlist.
• envc.never_vars(blocklist) — no var name read is in blocklist.
• envc.never_var_prefix(prefix) — no var name starts with prefix.
• envc.env_reads_at_most(count) — at most count reads occur.

Prefer only_vars when the needed variables are small and explicit (strongest). never_var_prefix("SECRET_") is a convenient blanket veto.

Example

import clauz3
from tools.env.trusted import contracts as envc
from tools.env.trusted.effects import read_env


@clauz3.guarantee(envc.only_vars(["GITHUB_REPO", "OPENAI_BASE_URL"]))
@clauz3.guarantee(envc.never_var_prefix("AWS_"))
def main() -> None:
    repo = read_env("GITHUB_REPO")
    base = read_env("OPENAI_BASE_URL")

Tests

clauz3 test stdlib:env

tests/cases/*_pass.py must prove; tests/cases/*_fail.py must not.

Source

src/clauz3/stdlib/env/tools/env/trusted/effects.py

"""Trusted environment-variable read effect.

``read_env`` returns the named variable's value, or the empty string if
unset. Carries the ``read`` and ``env`` markers so contracts in
``contracts.py`` can constrain *which* variables a program may read —
the primary credential-exfil guard for any agent that touches secrets
via the environment (the conventional shape for API keys).
"""

import os

import deal


@deal.pre(lambda name: len(name) > 0, message="env var name must be non-empty")
@deal.has("read", "env", "global", "trusted")
def read_env(name: str) -> str:
    """Return the value of env var ``name``, or the empty string if unset.

    Recorded under the ``read`` and ``env`` markers. The contract layer
    can restrict reads by name allowlist / blocklist or a total count.
    """
    return os.environ.get(name, "")

src/clauz3/stdlib/env/tools/env/trusted/contracts.py

"""Environment-variable read policies built from generic trusted effect facts.

Env reads carry the ``read`` and ``env`` markers. These contracts let an
agent state which environment variables it may inspect — the canonical
credential-exfil guard for any program that touches API keys or other
secrets via ``os.environ``.

Use ``only_vars(allowlist)`` when the set of needed variables is small and
explicit (the strongest guarantee). Use ``never_vars(blocklist)`` when
specific variables are known-sensitive and the program needs flexibility
otherwise. Use ``no_env_reads()`` when the program should not touch the
environment at all.
"""

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

EnvRead = effect("read_env")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about env-read effects."""
    return core_no_guarantees()


@contract
def no_env_reads() -> ContractSpec:
    """Guarantee the program reads no environment variables."""
    return EnvRead.empty()


@contract
def only_vars(allowlist: list[str]) -> ContractSpec:
    """Guarantee every env-var name read is in ``allowlist``."""
    return EnvRead.all(lambda e: e.name in allowlist)


@contract
def never_vars(blocklist: list[str]) -> ContractSpec:
    """Guarantee no env-var name read is in ``blocklist``."""
    return EnvRead.all(lambda e: e.name not in blocklist)


@contract
def never_var_prefix(prefix: str) -> ContractSpec:
    """Guarantee no env-var name read starts with ``prefix``.

    Useful for blanket prefixes like ``SECRET_`` or ``AWS_`` without
    enumerating every variable individually.
    """
    return EnvRead.all(lambda e: not e.name.startswith(prefix))


@contract
def env_reads_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` env-var reads occur."""
    return EnvRead.count() <= count

All cases

Browse the full set on the all-cases page.