Composite GitHub Actions for estate-wide CI/CD auditing. They are run by
the reusable workflow .github/workflows/main-estate-audit.yml. Each
repository calls that workflow from a ten-line caller; it does not copy
it (see Consuming it).
The audit reports five component checks, one check run each:
| Check | Gates |
|---|---|
|
required-files · spdx-license · affirmation · referencing |
|
code-hygiene · formatting · linguist · secrets · vaulted-tokens |
|
manifest · recipes-set |
|
idris2-abi · zig-unified-api-adapter · proof-runner · boj-cartridge |
|
the nine advisory gates below; this check cannot fail, by design |
Within a component every gate runs even after an earlier gate fails, so one push reports every failing gate. Before this change one job ran all 26 in sequence, and the first failure hid the rest behind "estate-audit: failing after 8s".
Published 2026-08-07. Defects (1)–(3) are fixed and verified against two live estate repositories; (4) is partly fixed; (5) is closed by removing the stubs from the workflow; (6) is open.
Before wiring this into a repository, read Known defects and Consuming it.
Of 26 actions, 15 can fail a build and 11 cannot — and the 11 are not one kind of thing. Conflating them was the original error.
| Class | Actions | Meaning |
|---|---|---|
Enforcing (15) |
affirmation · boj-cartridge · code-hygiene · formatting · idris2-abi · linguist · manifest · proof-runner · recipes-set · referencing · required-files · secrets · spdx-license · vaulted-tokens · zig-unified-api-adapter |
Can fail. A green tick means something. |
Advisory (9) |
badges · contractile-validation · custom-tools · gitsea · hosting · metrics · tests-benches · trust-humans · www-compliance |
Do real work, warn on genuinely soft findings. Failing the estate over a missing Keybase link would be worse than not checking. |
Unimplemented (2) |
prat · semantic-audit |
Stubs. Not referenced by the audit workflow. See (5). |
The four language gates added 2026-10-14 (Rust CI, Creusot, SPARK, miniKanren)
are enforcing by construction — every check.sh exits 1 on a defect and 2
when no check could be performed — and are classified tier by tier in
Language gates below.
formatting and recipes-set moved out of the toothless column;
the remaining advisory nine are advisory by design, which is
defensible — provided nobody reads their green tick as a guarantee.
Renaming them *-advisory would settle that permanently.
Verify at any time:
for a in actions/*/; do
grep -q 'exit 1' "$a/action.yml" && echo "ENFORCE $(basename $a)" || echo "advise $(basename $a)"
doneA gate that cannot fail is worse than no gate, because it is credited as assurance. The advisory 13 should either grow teeth or be renamed so nobody reads their green tick as a guarantee.
1. FIXED — code-hygiene-check scanned for the word, not the
marker. It ran one case-insensitive, unanchored git grep over the
whole tree, so “admit” matched “admitted”, “sorry” matched
ordinary English, any document discussing a marker failed, and
believe_me failed repos whose sanctioned axioms are their declared
trusted base. Measured 112 matching files in one repo and 313 in
another. Now two scans with different semantics — debt markers
case-sensitive and whole-word in source only; circumventions in proof
languages only, with comments filtered. Repos may exempt paths via
.cicd-hygiene-allow. Result: 112 → 2 and 313 → 3, all true
positives.
2. FIXED — required-files-check manufactured filler. Presence-only
checking meant the cheapest way to pass was template boilerplate, and
that is exactly what happened in the estate. It now checks presence,
then format, then substance: documents need real content and no
placeholders, ARCHITECTURE must name a directory that actually
exists, and MAINTAINERS must mention the repository owner — which
catches a template shipping its author’s handle. CODEOWNERS is
judged on whether it assigns an owner, not on length.
3. FIXED — the suite contradicted itself. required-files-check
hard-failed a repo for lacking GOVERNANCE.md while
formatting-check warned that same file should be .adoc.
Required-files now accepts every policy-legal form, and formatting-check
owns the preference. Verified: a repo passes both gates with .adoc
(silently) or with .md (with a nudge).
4. PARTLY FIXED — the toothless column is down from 13 to 11, and now
triaged. recipes-set was a stub that printed “Checking Justfile
syntax…” with the command commented out and then declared success; it
now parse-checks Justfiles and Makefiles and fails on a file that does
not parse. formatting gained teeth in (3). The nine remaining
advisories are advisory by design and defensible; the honest fix for
them is a rename to *-advisory, not teeth.
5. CLOSED — two actions are unimplemented stubs, and the workflow no longer runs them.
-
semantic-auditis pureechowith “Placeholder for actual invocation”; its real body iscicd-squabbler audit --semantic, andcicd-squabblerdoes not exist yet. It cannot be implemented, only parked. -
pratclaims to validate “PRAT testing”, but PRAT is defined nowhere in the estate — a search of every repository turns up only further copies of the workflow that calls it. Its current check passes any repository that has atests/directory or contains the letters “prat” anywhere. It cannot be honestly implemented until somebody says what PRAT is.
A stub that prints success cannot be credited as assurance, so neither
step is in main-estate-audit.yml any more. The two directories stay
under actions/ for now, for two reasons. Repositories still running a
pre-caller copy of the workflow reference them by path. And
tests/lock-transitive-closure.sh requires that the SHA the workflow
pins serves the whole actions/ tree at HEAD. Move them to draft/
once the estate runs the caller (see Consuming it).
6. OPEN — six actions use bare git grep with no path restriction
(idris2-abi, metrics, secrets, spdx-license,
vaulted-tokens, zig-unified-api-adapter) and may inherit a milder form of
defect (1).
An earlier rollout_estate.sh copied the whole workflow into 199
repositories. Each copy froze at whatever cicd-suite commit its
actions.lock held. That is why a gate fixed here kept failing
downstream. The composite-shell fix to required-files (#32, 2026-09-22)
had still not reached hyperpolymath/marches on 2026-10-14, because its
lock held 5a10b72, the commit before it. The caller replaces those
copies.
The workflow now has permissions: contents: read and pins
actions/checkout and every gate by full SHA.
A repository calls the audit; it does not copy it. Three pieces:
-
templates/estate-audit-caller.ymlbecomes.github/workflows/main-estate-audit.yml, with__CICD_SUITE_SHA__replaced by a full cicd-suite commit SHA:jobs: estate: uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@<40-hex sha> # cicd-suite main
Pin a full SHA, never
@mainor a tag: the account enforcessha_pinning_required, and@mainwould silently change the gate in every consuming repository at once. -
The caller must be de-onboarded from the repository’s
actions.lock. Onboarded, a cross-repository reusable-workflow call startup-fails with zero jobs.scripts/deonboard-estate-audit.sh <repo>removes the entry and prunes the dependencies only it reached, comparing owner and repository names case-insensitively as GitHub does. It is the estate-audit entry point toscripts/deonboard-workflow.sh, the one implementation every de-onboard goes through. It needs mikefarahyqv4, and it is idempotent. It refuses anyactions.lockschema it has not been tested on;tests/deonboard-lock-schemas.shholds one fixture per supported schema (v0.0.2, v0.0.3) and runs each through both entry points. -
templates/track-estate-audit.ymlbecomes.github/workflows/track-estate-audit.yml. Weekly, it opens a PR that moves the pin to cicd-suite HEAD; that PR’s own audit run is the check. It needs anAUTOMATION_TOKENsecret (a fine-grained token on that repository with Contents, Pull requests and Workflows set to read/write), becauseGITHUB_TOKENmay not write under.github/workflows/. Its oneuses:isstep-security/harden-runnerat a full SHA (egress to GitHub only); a repository that carriesactions.lockmust add that record (gh actions-lock) or the first run dies at Set up job.
rollout_estate.sh does all three for every local estate clone. It
writes files and does not commit them.
Added 2026-10-14. Four reusable workflows, consumed exactly like the estate
audit (a thin caller at a full SHA, de-onboarded from actions.lock), and
each built so that its oracle has demonstrably said no before its green is
credited.
| Reusable | Check contexts (caller job id, then job name) | Oracle |
|---|---|---|
|
|
cargo, every call |
|
|
Creusot at a pinned release. A planted FALSE contract must be refused and a planted TRUE one proved before the caller’s crates are proved; otherwise the verdict is VOID (exit 2), never green. |
|
|
standards' SPARK Theatre Gate (claims side, called at a pin, not copied)
plus GNATprove at pinned GNAT/GNATprove versions via Alire,
|
|
|
The relations are RUN by the interpreter their dialect names (guile, Chez, racket); relations with no goal-level test fail; impure operators are listed (enforceable); a claim with no relations is named. |
Why. From 2026-09-29 every rust-ci / Cargo check + clippy + fmt
calling standards' rust-ci-reusable.yml at a pre-fix SHA died in six
seconds: the reusable pinned dtolnay/rust-toolchain by commit and
passed no toolchain:, and a SHA ref carries no channel
(plasma-parser-writer#105). The fix landed upstream; the callers stayed
pinned behind it. actions/rust-ci-check/resolve.sh now computes the
channel before any action runs and refuses an empty one, and the
previous gate’s silent holes are closed: cargo test --all-targets
never ran a doctest, nothing denied rustc warnings outside clippy,
cargo doc never ran, the declared rust-version was never built,
and no supply-chain check ran unless opted in.
Tiers. Within each gate the theatre tier (a claim with nothing behind
it) and the oracle tier (the prover or interpreter run) are enforcing and
exit 1; the hollow and purity tiers warn by default and become
enforcing through an input (enforce_hollow, enforce_zero_contract,
enforce_purity, enforce_claims), mirroring standards' SPARK T2.
A tree with nothing to gate gets a ::notice:: that nothing ran — never a
tick read as assurance. A missing tool is exit 2, "no check was performed".
How the scripts are pinned. Each reusable job reads the caller’s own uses:
line back out of the caller’s checked-out workflow file (GITHUB_WORKFLOW_REF
names it; inside a reusable the github context is the caller’s), checks this
repository out at that SHA into .cicd-suite/ and runs actions/*-check/check.sh from there, after
scripts/verify-suite-checkout.sh has proved the checkout is that
commit. A caller pinned at a SHA runs exactly that commit’s scripts, with
no second pin to drift and no repin commit after a change to actions/.
The caller’s tree is read through git ls-files, so the untracked
.cicd-suite/ is invisible to it.
Self-test. .github/workflows/language-gates-self-test.yml runs each
gate’s test.sh: a fixture, a planted defect per claim, the exact
composite shell, and a mutant where one applies. The prover tiers are
exercised against stand-in oracles there; the planted controls in the
check scripts exercise the real provers on every live run.
Consuming. templates/rust-ci-caller.yml, creusot-gate-caller.yml,
spark-gate-caller.yml and kanren-gate-caller.yml become
.github/workflows/<name>.yml with __CICD_SUITE_SHA__ replaced;
scripts/deonboard-workflow.sh <repo> <workflow-path> de-onboards each
(the estate-audit script now delegates to it);
templates/track-estate-audit.yml moves every cicd-suite pin weekly by
PR. rollout_language_gates.sh does all of it per clone, by what the
tree contains. Keep the caller job ids above: they are the context strings
branch rules require.
Not yet witnessed live (2026-10-14). The Creusot and GNATprove install
steps and the exit-code contract of cargo creusot prove and
gnatprove --checks-as-errors=on were validated against the tools'
documentation and stand-ins, not against a live runner. The planted
controls are the safeguard: if either prover cannot refuse a false
contract on the runner, the gate reports VOID rather than green. The
first live subject for SPARK is cicd-squabbler’s
spark/squabble_gate.gpr; no repository in the first rollout carries
Creusot obligations yet.
Two constraints are evaluated in the caller’s repository, so nothing in this repository’s own CI can witness them; both are now guarded here.
-
Actions policy. The estate’s GitHub Actions policy admits actions that are hyperpolymath-owned, GitHub-made, Marketplace-verified, or on a short pattern list. A reusable that uses anything else startup-fails for every caller with "The action … is not allowed" — which is how
EmbarkStudios/cargo-deny-actionkilled the first live Rust gate caller (plasma-parser-writer#108, 2026-10-19) while the Creusot gate from the same commit ran. The gates now use onlyactions/,github/,hyperpolymath/*,dtolnay,swatinem,goto-bus-stopandtaiki-e, every one at a full SHA, andtests/gate-action-owners.sh(run by the self-test workflow) refuses any other owner or a tag pin. cargo-deny is installed throughtaiki-e/install-action; Alire is a sha256-pinned release binary rather thanalire-project/setup-alire, which also nested floating@v4tags. -
Callee lock. Since about 2026-10-15 GitHub validates a called reusable against the callee repository’s
actions.lockat the called SHA and rejects a dependency record whoseref:is its own commit SHA ("invalid lockfile pin"). The gate workflows are deliberately not keyed in this repository’s lock, and that resolves (witnessed: the Creusot gate on plasma-parser-writer#108). The SPARK gate’s nested standards theatre gate is pinned at standards75bd599, the first standards commit whose lock passes that validation; hypatia’s PIN-003 lists the 545 that do not. -
Consumers with a lock-sync gate. A repository whose CI requires every job-level reusable ref to be keyed in its own
actions.lockwith a transitively closeddependencies:section (cicd-squabbler’sscripts/check-lock-sync.sh) cannot de-onboard the caller as the templates assume. Such a repository onboards instead: onehyperpolymath/cicd-suite@<sha>record whoseuses:is the union of what the called gates use at that SHA, plus a record for each of those copied from a lock GitHub accepts, with the tag — never the SHA — asref:. cicd-squabbler#135 is the worked example (for its standards callers); gitbot-fleet’sscripts/fix-lock-self-sha-refs.shandscripts/lib/action-ref-tags.tsvcarry the tag map.
Code MPL-2.0, prose CC-BY-SA-4.0. See LICENSE.