posts: part 3 — the policy is the part that moves (closes #443)

[williamzujkowski]

Part 3 of the agent-controls series, closing #443. Implementation first: the
code was written and proving before a word of the post was drafted, which is the
series' standing promise and — after a ninety-post audit of claims that outran
their evidence — not a promise I wanted to break on the way out.

Backed by oscal-agent-controls#1.

The thesis

Parts 1 and 2 assume the policy is fixed. Part 2's proof quantifies over every
tool call and quietly holds the policy constant — which is exactly the variable
that moves for an actor whose trustworthiness changes while it runs.

What was verified before writing

I fetched all four IETF drafts rather than trusting the issue's summary, which
warned that its own readings were second-hand. Both load-bearing claims hold:

The policy_id defect is real. The draft defines it as "a string that
serves as an OPA policy reference and MUST match a registered policy in the AS"
— quoted verbatim in the post. Every integrity mention in the document is a JWS
signature over the token or the confirmation record. Nothing covers the policy
body the identifier resolves to. OSCAL's implemented-requirement has the same
shape, and the parallel is what bridges this post back to part 1.

Demotion genuinely does not exist. revoke/revocation occur 13 times
across the four drafts — 10 in one, 3 in another, zero in the remaining two.
demote, downgrade, step-down: zero, in all four.

Two corrections to the issue as filed: it says six drafts were read but lists
four, so the post claims four. And its "every draft models grant and revoke" is
too weak — two of the four do not model revocation either.

What now runs

• verify/Authority.dfy — authority modes, digest-bound grants, demotion
• verify/authority.rego + tests — independent twin
• gate/monitor.py — Authority, demote(), decide_bound(), policy_digest()
• verify/difftest/authority.py — 324 cases, three implementations, all agree

Six lemmas discharged, including DemotionCannotWiden and GrantBoundToPolicyBody.
Gate status: 26 Dafny obligations, 12 OPA tests, 13 pytest, both difftests green.

The best paragraph is a failure

DemotionTakesEffectImmediately did not verify on the first attempt. The
property was over-claimed — it needed a digest-match precondition, because when
the policy body has also rotated the call denies for a different reason.

Every test I would have written holds the policy constant and varies the mode,
which is precisely the case where my wrong claim is true. The post leads its
proof section with that rather than with the five lemmas that passed, because it
is the honest argument for the method: the prover objects when your model of
your own system is slightly wrong, at the moment you are most confident it isn't.

Two things I corrected in my own draft

Dated 2026-08-25 initially. That is a week in the future, which is the same
impossible-date defect the archive audit spent weeks removing. Re-dated to today.

Wrote "eleven times" for the revocation count, which came from grep -c —
lines containing a match, not occurrences. The real figure is 13. Corrected, and
the post now states what was actually measured.

Voice check clean, no banned words. Part 2 links forward.

[github-actions]

❌ Link Validation Results

• Total Links: 960
• Broken Links: 36
• Status: failed

View Full Report

Link Validation Report

Generated: 2026-08-19 03:50:37

Executive Summary

• Total Links Checked: 1501
• Valid Links: 1147 (76.4%)
• Broken Links: 44 (2.9%)
• Redirects: 0
• Requires Manual Review: 38
• Auto-Fixable: 1

Issue Breakdown

Issue Type	Count	Percentage
connection_error	197	13.1%
None	1147	76.4%
http_403	98	6.5%
not_found	18	1.2%
dns_error	26	1.7%
http_400	7	0.5%
timeout	3	0.2%
http_503	2	0.1%
http_401	1	0.1%
http_429	1	0.1%
http_402	1	0.1%

Top Affected Domains

Domain	Broken Links	Total Links
vault.example.com	5	5
example.local	4	4
raw.githubusercontent.com	4	5
wazuh-manager:55000	2	2
vaultwarden:80	2	2
www.intelrealsense.com	2	2
docs.vllm.ai	2	2
culorijs.org	1	3
azure.microsoft.com	1	4
climatemodeling.science.energy.gov	1	1

Repair Statistics

• High Confidence Fixes: 1
• Medium Confidence Fixes: 5
• Low Confidence Fixes: 0
• No Fix Available: 38

Files with Most Issues

File	Broken Links	Total Links
2025-09-01-self-hosted-bitwarden-migration-guide.md	8	19
2025-11-05-siem-homelab-wazuh-graylog-comparison.md	4	22
2026-07-23-agent-controls-as-oscal.md	4	11
2025-03-10-raspberry-pi-security-projects.md	3	8
2024-09-25-gvisor-container-sandboxing-security.md	3	45
2025-12-10-homelab-security-dashboard-grafana-prometheus.md	2	15
2025-10-13-embodied-ai-robots-physical-world.md	2	32
2025-10-29-privacy-first-ai-lab-local-llms.md	2	28
2025-08-09-ai-cognitive-infrastructure.md	2	24
2026-07-19-oklch-terminal-themes.md	1	11