Keel
Grounding report.
Every verification edge in keel, classified by who produces the signal and whether the actor being verified can write to that producer.
| target | keel |
|---|---|
| revision | ec00242c384a1ecd0439baf47adb3bea97da22c1 |
| generated | 2026-07-25T22:21:07.165663Z |
anchored / (anchored + self_referential + unknown) = 14 / 21
Coverage (judged)
| node kind | judged |
|---|---|
| ci_step | 27 |
| script | 17 |
ε-audit — not run
No verdict in this report carries a readable audit block, so nothing was re-decided and there is no agreement rate to report. This is not agreement, and it is not full agreement either: a rate over zero comparisons would state a measurement that was never taken. (“Readable” is load-bearing: a block can be present and state no comparison, and this state covers that too — see below if so.)
Scope. Keel measures the shape of verification, not its quality. A repo can be 100% anchored with terrible tests. Anchoring says the signal comes from outside; it does not say the signal is sufficient.
Node graph — 44 node(s), in gather order
anchored — 14
The signal is grep matching committed bytes, so a contributor who commits a machine-specific path cannot make the scan report clean without editing scripts/portability-check.sh itself. The same script runs in portability.yml on a fresh ubuntu-latest checkout with none of the author's tooling present, and that job is now a REQUIRED status check, so a non-zero exit blocks the merge. Documented limit: the oracle (which paths count, and the 80-file exemption list) is authored in-repo.
producer bash + grep -nE scanning the actual bytes of every file in `git ls-files`, with the script's fail flag driving exit 1 — actor can write to it: no
- Makefile: portability-check -> scripts/portability-check.sh
- .github/workflows/portability.yml:25 runs the same script
- ruleset 19744979 requires "no machine-specific paths"
decided by agent · confidence 0.85
The exit code comes from the interpreter reading files on disk, so someone adding a raw literal cannot make the scan report clean without editing scripts/design-audit.py. test.yml:93 invokes THIS target, and test (ubuntu-latest) is a required check, so this is the edge that blocks the merge rather than a target that could have. Documented limits: the rules are authored in-repo and checks 1-2 carry an `audit-ok:` per-line escape hatch.
producer python3 executing design-audit.py — regex scans and byte comparisons over the real governed files, returning 1 when the failures list is non-empty — actor can write to it: no
- .github/workflows/test.yml:93 "run: make design-audit"
- ruleset 19744979 requires "test (ubuntu-latest)"
- observed: 15 governed file(s) clean
decided by agent · confidence 0.85
Routed since ec00242. test.yml:82 now runs `bun run test` rather than a second copy of `bun test`, so this declaration IS the command the required check executes: the runtime decides the exit code and a red blocks the merge. Before the route the same two commands lived in two places and only the workflow copy gated anything, which made this node a statement of intent — the corpus classified it self_referential at 44f7e8d6 for exactly that reason. THE DOCUMENTED LIMIT is unchanged and is the honest one: only the EXECUTION axis is anchored. The oracle is authored in-repo beside the implementation, so a green run proves the code does what these tests say, not that they say the right thing.
producer the Bun test-runner process executing 297 tests on a runner the PR author does not control — reached THROUGH this declaration — actor can write to it: no
- package.json: "test": "bun test"
- .github/workflows/test.yml:82-83 — run: bun run test
- ruleset 19744979 requires test (ubuntu-latest) and test (macos-latest)
decided by agent · confidence 0.85
Routed since ec00242: test.yml:85 runs `bun run typecheck`, so the declared script is the edge the required check executes. A type error is decided by tsc reading the source and cannot be argued into a zero exit. Limit: it checks type consistency, not behaviour, and the annotations are authored in-repo — an internally consistent wrong type still passes.
producer the TypeScript compiler analysing the tree — reached THROUGH this declaration — actor can write to it: no
- package.json: "typecheck": "tsc --noEmit"
- .github/workflows/test.yml:85-86 — run: bun run typecheck
decided by agent · confidence 0.85
`--frozen-lockfile` is what separates this from a plain install: the resolver will not refresh a stale lock, it exits non-zero, so the step is a falsifiable assertion that two committed files agree. An author who edits a dependency and forgets to regenerate the lock cannot make this pass without changing the tree. It runs in a required check, so the red blocks the merge. Documented limit: what is anchored is manifest/lock agreement and registry reachability — nothing about whether the code works.
producer Bun's resolver comparing bun.lock against package.json and refusing to proceed on a mismatch — actor can write to it: no
- .github/workflows/test.yml:69-70 — run: bun install --frozen-lockfile
- ruleset 19744979 requires test (ubuntu-latest) and test (macos-latest)
decided by agent · confidence 0.85
The runtime decides pass or fail by executing 297 tests, and no prose in the repo talks a failed assertion into a zero exit. This is now the edge that blocks the merge: it runs on a fresh ubuntu and macOS runner and both legs are REQUIRED status checks under ruleset 19744979, so a non-zero exit cannot be merged past. THE DOCUMENTED LIMIT, and it is the honest one: only the EXECUTION axis is anchored. The oracle is authored in-repo alongside the implementation, so a green run proves the code does what these tests say — not that the tests say the right thing.
producer the Bun test-runner process — a failed expect() sets the process exit code, on a runner the PR author does not control — actor can write to it: no
- .github/workflows/test.yml:82-83 — run: bun run test
- ruleset 19744979 required_status_checks: test (ubuntu-latest), test (macos-latest)
- observed: 297 tests, 296 pass / 1 skip / 0 fail
decided by agent · confidence 0.9
A type error is decided by tsc reading the source; it cannot be argued out of a non-zero exit. Runs in both required legs, so it gates the merge. Documented limit: it checks type consistency, not behaviour — and the types are authored in-repo, so a wrong annotation that is internally consistent still passes.
producer the TypeScript compiler performing deterministic analysis of the tree — actor can write to it: no
- .github/workflows/test.yml:85-86 — run: bun run typecheck
decided by agent · confidence 0.9
Executed analysis of bytes on disk on a fresh runner, inside a required check. Mutation-proven in this repo's history: injecting a raw hex literal into a <style> block flipped the target red and reverting restored green. Documented limit: the rules and the `audit-ok:` escape hatch are authored in-repo, so the SCOPE oracle sits inside the write boundary even though the measurement does not.
producer python3 executing design-audit.py over the real governed files, exit 1 on any failure — actor can write to it: no
- .github/workflows/test.yml:93-95 — if ubuntu, run: make design-audit
decided by agent · confidence 0.85
The step recomputes the ratio from the stored verdicts and throws if the stored `grounding` block disagrees, and separately throws if any verdict carries no `writeBoundary.argument`. Both are executed comparisons whose exit code the runtime decides — a fixture edited into disagreeing with itself turns this red. It runs in a required check. Limit: it verifies internal consistency of the fixture, not that any verdict in it is correct.
producer a Bun one-liner recomputing groundingRatio() from the fixture's own verdicts and throwing on disagreement — actor can write to it: no
- .github/workflows/test.yml:100-113
decided by agent · confidence 0.85
gather is deterministic and the runtime decides the exit code, so a PR that adds or removes a verification edge cannot leave reports/keel-current.json describing a tree that no longer exists — which is exactly what happened to the published 0.357, stale by 21 commits while asserting a defect that had been fixed. The oracle is a committed file the PR may change, and that is the property rather than a hole: it can be moved, but not silently. Runs inside a required check. THE LIMIT, and it must be stated: this proves COVERAGE is current, never that any VERDICT is. Classification is agentic and CI has no agent; a probe-only run emitting a ratio over whatever the cache decided would be the shoppable move under another name, so this edge deliberately emits no ratio at all.
producer bun re-running gather.ts at HEAD and comparing the edge set against the committed report, throwing on any difference — actor can write to it: no
- .github/workflows/test.yml:140-171
- keyed on (file, kind, name), not Node.id — ids embed line numbers and would churn
- ruleset 19744979 requires "test (ubuntu-latest)"
decided by agent · confidence 0.9
grep matching real file contents on a clean checkout that has none of the maintainer's tooling — the runner is outside the write boundary of anything in this repo, so a pass here is an observation rather than a local assertion. "no machine-specific paths" is a REQUIRED status check, so a hit blocks the merge. Limit: the exemption list (80 files) is authored in-repo, so the scope is co-authored even though the scan is not.
producer bash + grep scanning committed bytes, with the script driving exit 1 — actor can write to it: no
- .github/workflows/portability.yml:25-26
- ruleset 19744979 requires "no machine-specific paths"
- observed: scanned 278 tracked files, 80 exempt
decided by agent · confidence 0.85
Six hooks are actually EXECUTED on a bare clone with no skills and no bstack installed, and the shell's exit status decides. A hook that breaks on a machine without the maintainer's environment cannot be talked into passing. Required check, so it blocks the merge.
producer bash executing each committed hook with an empty JSON payload; a non-zero exit fails the step under set -euo pipefail — actor can write to it: no
- .github/workflows/portability.yml:37-55
- ruleset 19744979 requires "hooks resolve on a bare clone"
decided by agent · confidence 0.85
The strongest edge in this repo, because it asserts BOTH directions: a force-push must exit 2 and an ordinary push must exit 0. Asserting only the block would pass against a hook that denies everything, and the step says so in its own comment. Two executed invocations, two compared exit codes, on a fresh runner, inside a required check.
producer bash running control-gate-hook.sh twice and comparing both exit codes — actor can write to it: no
- .github/workflows/portability.yml:57-72
decided by agent · confidence 0.85
The hook is really executed in an environment missing its optional dependency, and the shell's exit status decides whether it degraded gracefully. A hook that hard-fails without bstack turns this red, and it is a required check.
producer bash executing .githooks/pre-commit on a clone with no bstack present — actor can write to it: no
- .github/workflows/portability.yml:81-82
decided by agent · confidence 0.85
self_referential — 7
The oracle is paperwork against paperwork: the checks are of the form "a `### P-N` section exists in AGENTS.md" and "a matching `| P-N |` row exists in CLAUDE.md". Both files are in the tree of the PR being verified, so the way to make the gate green is to type the row. The runtime honestly produces the exit code, but the actor authored both sides of the comparison.
producer bstack doctor.sh --strict comparing AGENTS.md against CLAUDE.md — actor can write to it: yes
- Makefile: bstack-check runs doctor.sh --strict
- CLAUDE.md and AGENTS.md are both author-written
decided by agent · confidence 0.85
The script opens only AGENTS.md and CLAUDE.md and compares them to each other: every `### P-N` must carry the literal strings **What**/**How**/**Why**/**Invariant**, and each must have a `| P-N |` row. Both documents sit in the tree the gate is verifying, so the fix for a red is always "write the missing prose". Doc validated against doc.
producer python3 bstack-primitive-lint.py comparing AGENTS.md section structure against CLAUDE.md table rows — actor can write to it: yes
- scripts/bstack-primitive-lint.py reads AGENTS.md and CLAUDE.md only
decided by agent · confidence 0.85
"This pattern recurred 3+ times" is established by matching a string a human typed into a ledger markdown file. The evidence and the claim are the same write. Additionally inert here: the Makefile documents that Keel promotes no primitives, so the ledger does not exist and the script fails on a missing file rather than on a real violation — which is why bstack-l3-trust deliberately does not wire it.
producer python3 bstack-rule-of-three.py regexing a ledger table in research/entities/ — actor can write to it: yes
- Makefile comment block: "G-L3-2 rule-of-three not run: no primitives are promoted in this repo"
decided by agent · confidence 0.85
A green aggregate: do not classify the wrapper, descend. Its only real child is bstack-primitive-lint, whose signal is AGENTS.md compared against CLAUDE.md — the same two files a governance PR edits. The three `@echo` lines cannot fail. So the aggregate is exactly as grounded as its one self-referential child.
producer an aggregate of one child, bstack-primitive-lint, plus three echo lines — actor can write to it: yes
- Makefile: bstack-l3-trust: bstack-primitive-lint, then three @echo lines
decided by agent · confidence 0.85
The step posts an authoritative-looking merge recommendation ("composite system unstable; do not merge" / "All gates pass") that a human reviewer may act on. Both the claim and its evidence are authored by this one job from constants in .control/rcs-parameters.toml — a file inside the PR's own tree, and itself one of the paths that triggers this workflow. The claim and the check are the same write.
producer actions/github-script rendering a verdict string built from this job's own step outputs — actor can write to it: yes
- .github/workflows/l3-stability.yml:83-123
- .control/rcs-parameters.toml is in-tree and is a trigger path
decided by agent · confidence 0.85
This is the only edge in the job that can turn red, so it is the gate — but descending it lands on the same actor-authored constants: exit 1 fires iff lambda_i <= 0 for numbers the PR author may edit in the same commit. Additionally it gates nothing today: this workflow is not among the required status checks, and it triggers only on governance paths.
producer the shell comparing steps.compute.outputs.status against "0" — actor can write to it: yes
- .github/workflows/l3-stability.yml:125-133
- ruleset 19744979 does not list any l3-stability check
decided by agent · confidence 0.85
It runs on a fresh runner inside a required check, so the EXECUTION is independent — but descend the aggregate and the oracle is doc-against-doc: AGENTS.md sections matched to CLAUDE.md table rows, both authored by whoever opened the PR. Independence of the runner does not rescue an oracle the actor writes; the way to make this green is to type the missing prose.
producer make bstack-l3-trust, which descends to bstack-primitive-lint comparing AGENTS.md against CLAUDE.md — actor can write to it: yes
- .github/workflows/portability.yml:78-79 — run: make BSTACK= bstack-l3-trust
- Makefile: bstack-l3-trust depends only on bstack-primitive-lint
decided by agent · confidence 0.85
not_a_check — 23
A long-running interactive development server. It has no terminal state, so it cannot report pass or fail about anything. Same shape as the framework-dev-server-script probe.
producer the Remotion dev server process, which runs until interrupted — actor can write to it: no
- video/package.json: "studio": "remotion studio"
decided by agent · confidence 0.85
The command exists to produce keel-explainer.mp4. Its exit status is consumed by nothing — no workflow invokes it and no other target depends on it — and success means "it rendered", never that any property of the repository holds. Closest shape in the library is artifact-publish-upload (not_a_check), not packaging-build-invocation, which is anchored only where a build acts AS A GATE. Named vacuousness: a broken composition would be caught by a human watching the video, not by this edge.
producer the Remotion/esbuild toolchain writing an output file — actor can write to it: no
- video/package.json
- no workflow references video/ (grep over .github/workflows)
decided by agent · confidence 0.85
The command exists to produce keel-pitch-60.mp4. Its exit status is consumed by nothing — no workflow invokes it and no other target depends on it — and success means "it rendered", never that any property of the repository holds. Closest shape in the library is artifact-publish-upload (not_a_check), not packaging-build-invocation, which is anchored only where a build acts AS A GATE. Named vacuousness: a broken composition would be caught by a human watching the video, not by this edge.
producer the Remotion/esbuild toolchain writing an output file — actor can write to it: no
- video/package.json
- no workflow references video/ (grep over .github/workflows)
decided by agent · confidence 0.85
The command exists to produce still.png. Its exit status is consumed by nothing — no workflow invokes it and no other target depends on it — and success means "it rendered", never that any property of the repository holds. Closest shape in the library is artifact-publish-upload (not_a_check), not packaging-build-invocation, which is anchored only where a build acts AS A GATE. Named vacuousness: a broken composition would be caught by a human watching the video, not by this edge.
producer the Remotion/esbuild toolchain writing an output file — actor can write to it: no
- video/package.json
- no workflow references video/ (grep over .github/workflows)
decided by agent · confidence 0.85
The output is the Makefile's own `## ` comments re-printed. Nothing about the repository is compared against anything, and the exit status is awk's formatting status, so no state of the world can flip it.
producer grep -hE over $(MAKEFILE_LIST) piped to awk, reformatting the ## doc-comments — actor can write to it: no
- Makefile: help target body is a grep|awk pipeline over MAKEFILE_LIST
decided by agent · confidence 0.85
The target's own doc-comment reads "always exits 0". A signal that cannot vary carries no information, so this is not_a_check by falsifiability rather than by content — the report it prints may be useful to a human, but no state of the world turns this red.
producer bstack doctor.sh, which the target documents as always exiting 0 — actor can write to it: no
- Makefile: "doctor: ## bstack primitive-contract compliance report (needs bstack; always exits 0)"
decided by agent · confidence 0.85
A rewriter, not an assertion — it makes the files agree rather than reporting whether they did. Same shape as a formatter that only rewrites. The checking counterpart is `make design-audit`, classified separately.
producer design-audit.py --fix-sync, which rewrites site/ token copies in place — actor can write to it: no
- Makefile: design-sync -> design-audit.py --fix-sync
decided by agent · confidence 0.85
The target answers a housekeeping question (dry-run) — which local branches already landed and which worktrees are orphaned — and prints the list. Control reaches an unconditional exit 0 at branch-janitor.sh:214, so no finding can turn it red. Nothing here asserts the repository is correct.
producer git plumbing (merge-base --is-ancestor, commit-tree + cherry) over origin/main — actor can write to it: no
- scripts/branch-janitor.sh:214 unconditional exit 0
decided by agent · confidence 0.85
The target answers a housekeeping question (--apply) — which local branches already landed and which worktrees are orphaned — and prints the list. Control reaches an unconditional exit 0 at branch-janitor.sh:214, so no finding can turn it red. Nothing here asserts the repository is correct.
producer git plumbing (merge-base --is-ancestor, commit-tree + cherry) over origin/main — actor can write to it: no
- scripts/branch-janitor.sh:214 unconditional exit 0
decided by agent · confidence 0.85
Provisioning: it places code or a toolchain on the runner. It can fail on infrastructure, but it asserts nothing about whether the repository is correct.
producer the actions/checkout@v4 action provisioning the runner — actor can write to it: no
- .github/workflows/l3-stability.yml — actions/checkout@v4
decided by agent · confidence 0.85
Provisioning: it places code or a toolchain on the runner. It can fail on infrastructure, but it asserts nothing about whether the repository is correct.
producer the actions/setup-python@v5 action provisioning the runner — actor can write to it: no
- .github/workflows/l3-stability.yml — actions/setup-python@v5
decided by agent · confidence 0.85
Provisioning — it fetches a dependency and exports BSTACK. It asserts nothing about this repository. Worth recording though it does not change the class: the clone is pinned to a mutable third-party HEAD and the enclosing job holds pull-requests: write, so a compromise upstream executes here. That is a supply-chain finding, not a grounding one.
producer git clone of https://github.com/broomva/bstack.git at whatever main points to — actor can write to it: no
- .github/workflows/l3-stability.yml:44-48 — git clone --depth 1, no ref or SHA
- .github/workflows/l3-stability.yml:27-29 — permissions: pull-requests: write
decided by agent · confidence 0.85
The Compute lambda step ends in a literal unconditional `exit 0` — `set +e` captures the real status into $GITHUB_OUTPUT and the step then always succeeds. A step that cannot vary asserts nothing, so it is not_a_check by falsifiability even though its captured value is meaningful downstream. The edge that CAN fail is "Set final status", classified separately. NOTE: the corpus judged this self_referential at 44f7e8d6, reasoning from the author-written constants; the `exit 0` is the more decisive structural fact and it moves the node OUT of the denominator, which is the shoppable direction — recorded here explicitly rather than silently.
producer a bstack shell script whose status is captured into a step output, followed by an unconditional `exit 0` — actor can write to it: no
- .github/workflows/l3-stability.yml — Compute lambda step body ends "exit 0"
decided by agent · confidence 0.7
The Run L3 rate gate step ends in a literal unconditional `exit 0` — `set +e` captures the real status into $GITHUB_OUTPUT and the step then always succeeds. A step that cannot vary asserts nothing, so it is not_a_check by falsifiability even though its captured value is meaningful downstream. The edge that CAN fail is "Set final status", classified separately. NOTE: the corpus judged this self_referential at 44f7e8d6, reasoning from the author-written constants; the `exit 0` is the more decisive structural fact and it moves the node OUT of the denominator, which is the shoppable direction — recorded here explicitly rather than silently.
producer a bstack shell script whose status is captured into a step output, followed by an unconditional `exit 0` — actor can write to it: no
- .github/workflows/l3-stability.yml — Run L3 rate gate step body ends "exit 0"
decided by agent · confidence 0.7
Provisioning for a deployment job. Asserts nothing about correctness.
producer the actions/checkout@v4 action provisioning the deploy job — actor can write to it: no
- .github/workflows/pages.yml — actions/checkout@v4
decided by agent · confidence 0.85
Provisioning for a deployment job. Asserts nothing about correctness.
producer the actions/configure-pages@v5 action provisioning the deploy job — actor can write to it: no
- .github/workflows/pages.yml — actions/configure-pages@v5
decided by agent · confidence 0.85
It ships an already-built directory. Same shape as artifact-publish-upload: transport, not assertion. Nothing about site/ is verified by uploading it.
producer actions/upload-pages-artifact packaging site/ into a Pages artifact — actor can write to it: no
- .github/workflows/pages.yml:29-31 — path: site
decided by agent · confidence 0.85
A deployment. It runs on push to main — after the merge — so it gates nothing, and success means "the bytes were published", not that they are right. The honest check on the deployed site is fetching its content, which this repo has done by hand but does not wire here.
producer actions/deploy-pages publishing the artifact to GitHub Pages — actor can write to it: no
- .github/workflows/pages.yml — on: push branches [main]
decided by agent · confidence 0.85
Provisioning. It places the source or the toolchain on a fresh runner; it makes no claim about the code.
producer the actions/checkout@v4 action provisioning the runner — actor can write to it: no
- .github/workflows/test.yml — actions/checkout@v4
decided by agent · confidence 0.85
Provisioning. It places the source or the toolchain on a fresh runner; it makes no claim about the code.
producer the oven-sh/setup-bun@v2 action provisioning the runner — actor can write to it: no
- .github/workflows/test.yml — oven-sh/setup-bun@v2
decided by agent · confidence 0.85
Provisioning. It asserts nothing about the code it checks out.
producer the actions/checkout@v4 action placing the source on the runner — actor can write to it: no
- .github/workflows/portability.yml — uses: actions/checkout@v4
decided by agent · confidence 0.85
Provisioning. It asserts nothing about the code it checks out.
producer the actions/checkout@v4 action placing the source on the runner — actor can write to it: no
- .github/workflows/portability.yml — uses: actions/checkout@v4
decided by agent · confidence 0.85
Provisioning. It asserts nothing about the code it checks out.
producer the actions/checkout@v4 action placing the source on the runner — actor can write to it: no
- .github/workflows/portability.yml — uses: actions/checkout@v4
decided by agent · confidence 0.85
Crystallization curve
Run economics