safety: make every central claim enforced by something that can fail - #111

Merged

bordumb merged 61 commits into

mainfrom

Aug 17, 2026

Commits on Aug 15, 2026

fix(safety): close fail-open paths and freeze Rust-owned vocabulary

bordumb
and
claude
committed
2ee0976
fix(corpus): converge three verifiers on absent-budget denial

bordumb
and
claude
committed
f5c3589
core: make root preservation a computed dimension and a real proof (UNSIGNED)
bordumb
committed
1a88ba3
product: let the signed receipt say "unknown", and sign it only after every gate
bordumb
committed
d735eda
product: rebuild auths-node on the verified kernel (UNSIGNED)
bordumb
committed
d82d57f
formal: repoint the assurance inventory at the renamed root theorem

bordumb
and
claude
committed
a85f6b7
core: make terminal budget coverage the kernel's own answer (UNSIGNED)

bordumb
and
claude
committed
ac5b968
formal: run the 31 ungated Kani harnesses and fix what they proved (UNSIGNED)

bordumb
and
claude
committed
f82cb08
formal: make attenuation dimension 11 expressible, then prove it (UNSIGNED)

bordumb
and
claude
committed
e21fb2c
test: make the effect axis a failing acceptance test in both bindings (UNSIGNED)
bordumb
committed
f34d37a
gate: detect mirrored and homonymous public exports (UNSIGNED)

bordumb
and
claude
committed
29b7bab
bindings/wasm: carry the error envelope, drop the reference machinery (UNSIGNED)
bordumb
committed
9e17ff8
bindings/python: make the pyo3 boundary a transport, not a tier (UNSIGNED)

bordumb
and
claude
committed
ad8e25b
bindings/typescript: one effect axis, and a WASM boundary that carries it (UNSIGNED)
bordumb
committed
5964279

Commits on Aug 16, 2026

product/mcp: let the profile name its own outcome, and TypeScript read it (UNSIGNED)
bordumb
committed
b4c6674
bindings/python: one vocabulary, one entry point per operation (UNSIGNED)
bordumb
committed
c04bd48
gate: repoint the semantic-freeze inventory at auths._service (UNSIGNED)
bordumb
committed
7031e3d
bindings/typescript: one vocabulary, one entry point per operation (UNSIGNED)
bordumb
committed
723a71f
bindings/typescript: delete the workflow layer's private effect axis (UNSIGNED)
bordumb
committed
a8a6ee9
gate: repoint the semantic-freeze inventory at the service entry point (UNSIGNED)
bordumb
committed
7e16b3d
chore: record the auths-profile-mcp dev-dependency in the lockfile (UNSIGNED)
bordumb
committed
443c328
verify: delete two surviving binding-local classification rules (UNSIGNED)

bordumb
and
claude
committed
cadbbb8
core: make budget expressiveness a declared profile property (UNSIGNED)
bordumb
committed
ef85a8b
bindings: one factory name per concept across both languages (UNSIGNED)

bordumb
and
claude
committed
b5a95d5
release: assign semantic versions for every identity this branch drifted (UNSIGNED)

bordumb
and
claude
committed
334e34c
chore(formal): regenerate qualification artifacts
github-actions[bot]
committed
c578427
style: cargo fmt (UNSIGNED)

bordumb
and
claude
committed
7b8571d
ci: fix the three failures from the first CI run (UNSIGNED)

bordumb
and
claude
committed
17038d9
ci: make auths-node build standalone, and regenerate the stale recipe doc (UNSIGNED)

bordumb
and
claude
committed
697bd99
demos: make the reference-stack smoke test say what failed (UNSIGNED)

bordumb
and
claude
committed
a91a4e2
demos: give the reference stack the trusted context it requires (UNSIGNED)

bordumb
and
claude
committed
26306e1
formal: bind the root-linkage temporaries so aeneas can translate them (UNSIGNED)

bordumb
and
claude
committed
4b91cd6
chore(formal): regenerate qualification artifacts
github-actions[bot]
committed
8acdf8b
ci: regenerate the architecture snapshot for the std feature edges (UNSIGNED)

bordumb
and
claude
committed
668f219
release: resync the freeze after the upstream formal regeneration (UNSIGNED)

bordumb
and
claude
committed
0f6e341
formal: close the refinement gap by regenerating the translation (UNSIGNED)

bordumb
and
claude
committed
3d8338f
chore(formal): regenerate qualification artifacts
github-actions[bot]
committed
6f3f667
formal: make mutation kills compiled theorems instead of prose (UNSIGNED)

bordumb
and
claude
committed
e94c688
formal: bound critical-extension payloads in the representation invariant (UNSIGNED)

bordumb
and
claude
committed
6b8ee8a
formal: name every scope dimension instead of nesting nine conjuncts (UNSIGNED)

bordumb
and
claude
committed
b355dd3
formal: make the attenuation projection carry its own certificate (UNSIGNED)

bordumb
and
claude
committed
71056b7
formal: bind every evidence artifact to its digest (UNSIGNED)

bordumb
and
claude
committed
422d4ce
formal: account for every upstream sorry, and keep evidence digests fresh (UNSIGNED)

bordumb
and
claude
committed
48d8572
demos: author the reference stack's authority offline (UNSIGNED)

bordumb
and
claude
committed
a7bb471
bindings: let a client carry a proof it already holds (UNSIGNED)

bordumb
and
claude
committed
273e9b6
demos: pass the required identity to the reference clients (UNSIGNED)

bordumb
and
claude
committed
f3fe4ee
demos: make the authored proof actually verify (UNSIGNED)

bordumb
and
claude
committed
aa2669c
demos: contain the authored grant inside the anchor's validity (UNSIGNED)

bordumb
and
claude
committed
90f86ad
ci: show why the node denied instead of only that it did (UNSIGNED)

bordumb
and
claude
committed
84fe447
formal: harden the assurance boundary across all eleven review items (UNSIGNED)

bordumb
and
claude
committed
7d584b3
chore(formal): regenerate qualification artifacts
github-actions[bot]
committed
ff0c73b
ci: close semantic and platform reliability gaps
bordumb
committed
d328756
fix: fail closed across clean-checkout CI
bordumb
committed
65e0a10
fix: verify signed receipts across replicas
bordumb
committed
fabeb55
fix: align reference recovery contract
bordumb
committed
299ed38

Commits on Aug 17, 2026