gh¶

A trusted clauz3 layer for running the GitHub CLI (gh) from a proved program, with verb, object, and repository policies an agent can prove before any command runs.

The effect is real, not a mock: gh shells out to the gh binary. The prover never runs its 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. Arguments are passed as an explicit vector (never a shell string), so no field is interpreted by a shell.

Every invocation has the shape gh <command> <action> <args...> --repo <repo>. Recording command (the GitHub object, e.g. pr) and action (the verb, e.g. view) separately is the policy surface a raw shell allowlist cannot express: read_only constrains the verb while only_commands and only_repo independently bound the object and the repository.

Install¶

clauz3 install stdlib:gh

This copies tools/gh/ into your project. Then prove a program against it:

clauz3 prove --trusted-root tools/gh/trusted plan.py

Effects¶

Import with from tools.gh.trusted.effects import gh:

gh(command: str, action: str, args: list[str], repo: str) -> str — run gh <command> <action> <args...> --repo <repo> and return its stdout. Precondition: command, action, and repo non-empty.

Contracts¶

Import with from tools.gh.trusted import contracts as gh_rules:

gh_rules.no_guarantees() — explicit null contract.
gh_rules.no_gh() — the program makes no GitHub-CLI calls.
gh_rules.read_only() — every invocation uses a read-only verb (READ_ONLY_ACTIONS: view, list, status, diff, checks).
gh_rules.only_commands(allowlist) — every command (object) is in allowlist, e.g. only_commands(["pr", "issue"]).
gh_rules.never_actions(blocklist) — no action (verb) is in blocklist, e.g. never_actions(["merge", "close", "delete"]).
gh_rules.only_repo(repo) — every invocation targets the owner/name slug repo.
gh_rules.only_owner(owner) — every targeted repository belongs to owner (matches any owner/<name> slug).
gh_rules.runs_at_most(count) — at most count invocations occur.

read_only, only_commands, and never_actions are name-set policies; only_repo is an equality policy and only_owner is a str.startswith prefix policy.

Example¶

import clauz3
from tools.gh.trusted import contracts as gh_rules
from tools.gh.trusted.effects import gh


@clauz3.guarantee(gh_rules.only_repo("cmungall/agent-deal"))
@clauz3.guarantee(gh_rules.only_commands(["pr", "issue"]))
@clauz3.guarantee(gh_rules.never_actions(["merge", "close", "delete"]))
def main() -> None:
    gh("pr", "view", ["42"], "cmungall/agent-deal")
    gh("pr", "comment", ["42", "--body", "looks good"], "cmungall/agent-deal")

Stacking guarantees confines the program to one repository, to pull requests and issues, and forbids the destructive verbs. A gh("pr", "merge", ...) or a gh("repo", "delete", ...) would fail the proof, as would any call against a different repository.

Tests¶

just -f tests/Justfile test

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

Source¶

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

"""Trusted GitHub-CLI effect: a real (non-mock) ``gh`` subprocess.

``gh`` runs a single GitHub CLI invocation of the shape
``gh <command> <action> <args...> --repo <repo>`` and returns its stdout. It
is recorded by name so the contracts in ``contracts.py`` can scope which
GitHub objects an agent may touch (``command``, e.g. ``pr`` / ``issue``),
which verbs it may run (``action``, e.g. ``view`` / ``merge``), and which
repository it may target (``repo``).

Splitting ``command`` and ``action`` is the genuinely useful policy surface a
raw shell allowlist cannot express statically: ``read_only`` constrains the
*verb* (no ``merge`` / ``close`` / ``delete``) while ``only_commands`` and
``only_repo`` independently bound the *noun* and the *repository*.

The body shells out via ``subprocess.run`` with an explicit argument vector
(never a shell string), so ``syscall`` is declared among its deal markers. The
prover never runs the body — it records each call as a fact and proves the
contract; the body runs only under ``clauz3 run``.
"""

import subprocess

import deal

import clauz3

DEFAULT_TIMEOUT_SECONDS = 120


@clauz3.requires(
    lambda command, action, args, repo: (
        len(command) > 0 and len(action) > 0 and len(repo) > 0
    ),
    message="command, action, and repo must be non-empty",
)
@deal.has("network", "io", "syscall")
@clauz3.trusted
def gh(command: str, action: str, args: list[str], repo: str) -> str:
    """Run ``gh <command> <action> <args...> --repo <repo>`` and return stdout.

    Arguments are passed as an explicit vector, so no field is interpreted by a
    shell. ``repo`` is always supplied as ``--repo`` so every call is scoped to
    a single repository, which ``only_repo`` / ``only_owner`` can then pin.
    """
    completed = subprocess.run(  # noqa: S603
        ["gh", command, action, *args, "--repo", repo],
        capture_output=True,
        text=True,
        timeout=DEFAULT_TIMEOUT_SECONDS,
        check=True,
    )
    return completed.stdout

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

"""GitHub-CLI policies built from generic trusted effect facts.

Every ``gh`` invocation is recorded as the ``gh`` effect with its
``command`` (the GitHub object, e.g. ``pr``), ``action`` (the verb, e.g.
``view``), and target ``repo`` (see ``effects.py``). These contracts let an
agent state which verbs it may run, which objects it may touch, and which
repository it may target.

``read_only`` is the headline guard: it pins every invocation to a fixed set of
inspection verbs, so an agent handed the GitHub CLI can browse pull requests,
issues, and runs but cannot merge, close, delete, or otherwise mutate the
remote.
"""

from tools.gh.trusted.effects import gh

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

Gh = effect(gh)

#: GitHub-CLI verbs that only read state. ``read_only`` pins every ``action``
#: to this set. Deliberately excludes mutating verbs such as ``create``,
#: ``edit``, ``merge``, ``close``, ``comment``, ``delete``, and ``ready``.
READ_ONLY_ACTIONS = [
    "view",
    "list",
    "status",
    "diff",
    "checks",
]


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


@contract
def no_gh() -> ContractSpec:
    """Guarantee the program makes no GitHub-CLI calls."""
    return Gh.empty()


@contract
def read_only() -> ContractSpec:
    """Guarantee every gh invocation uses a read-only verb.

    Pins each ``action`` to ``READ_ONLY_ACTIONS``, so the program cannot mutate
    any GitHub object (no ``merge`` / ``close`` / ``delete`` / ``edit`` ...).
    """
    return Gh.all(lambda e: e.action in READ_ONLY_ACTIONS)


@contract
def only_commands(allowlist: list[str]) -> ContractSpec:
    """Guarantee every gh command (the GitHub object) is in ``allowlist``.

    For example ``only_commands(["pr", "issue"])`` lets an agent work with pull
    requests and issues but not ``repo``, ``release``, ``secret``, ...
    """
    return Gh.all(lambda e: e.command in allowlist)


@contract
def never_actions(blocklist: list[str]) -> ContractSpec:
    """Guarantee no gh action (the verb) is in ``blocklist``.

    Useful to veto specific mutating verbs (``merge``, ``close``, ``delete``)
    while leaving the rest of the CLI available.
    """
    return Gh.all(lambda e: e.action not in blocklist)


@contract
def only_repo(repo: str) -> ContractSpec:
    """Guarantee every gh invocation targets the repository ``repo``.

    ``repo`` is the full ``owner/name`` slug passed as ``--repo``.
    """
    return Gh.all(lambda e: e.repo == repo)


@contract
def only_owner(owner: str) -> ContractSpec:
    """Guarantee every targeted repository belongs to ``owner``.

    Matches any ``owner/<name>`` slug, so an agent can range over one
    organization's repositories without naming each one.
    """
    prefix = owner + "/"
    return Gh.all(lambda e: e.repo.startswith(prefix))


@contract
def runs_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` gh invocations occur."""
    return Gh.count() <= count

All cases¶

Browse the full set on the all-cases page.