diff --git a/docs/decisions/0026-closed-world-accountability-as-a-scoped-design-objective.md b/docs/decisions/0026-closed-world-accountability-as-a-scoped-design-objective.md new file mode 100644 index 0000000..52a853a --- /dev/null +++ b/docs/decisions/0026-closed-world-accountability-as-a-scoped-design-objective.md @@ -0,0 +1,632 @@ +# 0026: Closed-World Accountability As A Scoped Design Objective + +Date: 2026-09-22 +Status: accepted 2026-09-23 as a scoped design objective and research plan +(revision 3, BDFL ruling). Revision 2 was rejected as written (BDFL ruling +2026-09-22); the non-bolt-on exclusivity claim is withdrawn. See Ruling. + +Recommendation only; the BDFL rules. + +## Verdict From The Independent Thesis Review + +> Closed-world accountability is a defensible design objective, but this +> record does not establish it as a property that cannot be bolted onto +> Rust. Its central inference confuses limitations of today's loosely +> assembled tools with limitations of an enforced Rust verification +> profile. It also grants Hum a trusted implementation boundary while +> repeatedly treating comparable Rust boundaries as disqualifying. + +Disposition: reject 0026 as the justification for a non-bolt-on property. +Retain closed-world accountability as a scoped design objective, and require +an enforced-Rust-profile comparison before using it to decide the +language-versus-toolchain investment. + +This revision accepts that disposition in full. The exclusivity claim is +withdrawn. What remains is the objective, a corrected evidence model, an +honest map of what Hum's decisions do and do not establish, and a symmetric +falsifier. + +## Evidence Labels + +Claims in this record are labeled: + +- **[Requirement]** — an accepted design decision. Binding, not yet + necessarily implemented. +- **[Implemented]** — behavior that exists in the repository today. +- **[Guarantee]** — an established guarantee, with its scope stated. +- **[External]** — established by targeted research (2026-09-22–23) + against primary sources. +- **[Inference]** — the author's engineering judgment. Argued, not proven. + +A citation to a design decision does not collapse these categories. + +## Context + +Backlog item 6 names the landscape's sharpest counterargument against Hum +as a language project: everything except the intent ladder could be bolted +onto rustc tomorrow as JSON output plus a linter. If intent sections turn +out to be expressible as Rust attributes or macros plus a linter, Hum's +language bet weakens to "a really good toolchain" **[Requirement]** +(docs/research/hum-improvement-backlog-2026-09-22.md §6). The item's +evidence bar: the record names the property, the bolt-on attempt that +fails, and what dies if the claim is wrong. + +Revision 2 argued the property was non-bolt-on. The independent thesis +review rejects that argument (see Verdict). This revision keeps +closed-world accountability as a design objective and replaces the +exclusivity claim with a harder question: which necessary part requires +different executable-language semantics rather than a compiler extension, +restrictions, contracts, or an execution boundary? + +## The Design Objective + +**Closed-world accountability:** for every obligation in a Hum program, the +compiler can say whether it was proved, bounded, or explicitly trusted — +and nothing escapes that account. **[Inference]** (design objective under +test; no longer claimed as non-bolt-on). + +Stated as a conditional guarantee rather than an absolute one: + +> Assuming the compiler, runtime and named host primitives implement their +> specified semantics, every accepted source operation and profile-defined +> obligation has a recorded disposition. + +That is useful. It is not an end-to-end theorem about arbitrary behavior +of the native executable. + +"For every obligation" needs an explicit denominator. A coherent account +needs five separate dimensions: + +1. **Obligation kind** — declared formal contract, compiler-generated + safety obligation, effect obligation, and so on. A compiler can + enumerate obligations generated by a specified language/profile; it + cannot infer that this enumeration captures all unstated intent. +2. **Evidence result** — proved, refuted, bounded, unknown, unsupported, + timeout. +3. **Runtime enforcement** — statically discharged, runtime-checked, or + unchecked. +4. **Scope** — the build inputs, target, and configuration the evidence + covers. +5. **Assumptions and trust dependencies** — what the evidence depends on + being true. + +Decision 0020 already illustrates why declared/derived origin, +verification outcome, and completion claims must remain separate fields +**[Guarantee]** (0020-adopt-termination-measures-and-loop-bounds.md). + +Completeness is relative to an explicit obligation-generating +specification. Unknown obligations must remain visible and trigger +rejection, runtime enforcement where appropriate, or an explicitly +authorized assumption. Automatically renaming everything unknown as +trusted would make the property vacuous. **[Inference]** + +## The Stronger Steelman: The Enforced Rust Profile + +Revision 2's steelman voluntarily combined tools and voluntarily confined +I/O — a fair description of today's practice, but not the strongest +opponent. The strongest opponent is a **mandatory, fail-closed Rust +compilation profile** backed by a controlled build and execution +environment **[External]**: + +> Control the compilation universe. Pin the compiler, target, features, +> configuration, dependencies, and build inputs. Reject unapproved native +> libraries, build scripts, and procedural macros; sandbox permitted +> build-time execution. Analyze the actual expanded program and bind +> evidence to the artifact subsequently executed. Choose verification tools +> deliberately: one principal verifier for the admitted subset, additional +> backends only through specified evidence interfaces. Enforce authority at +> the execution boundary. Make supply-chain changes admission decisions. +> Put one authoritative checker in front of release: it assigns obligation +> identities, checks coverage, records assumptions and proof dependencies, +> distinguishes bounded evidence from runtime enforcement, and refuses +> missing or stale evidence. + +Each mechanism is real: + +- **Build-time control.** Cackle checks dependency API and `unsafe` usage + and can sandbox build scripts, tests, and rustc itself (hence proc + macros) on Linux — with documented circumvention warnings, so it is a + component and a precedent, not sufficient enforcement by itself + **[External]** (cackle-rs/cackle README and CONFIG.md). +- **Deliberate verifier choice.** RefinedRust's foundational verification + of safe *and* unsafe Rust, with proofs checked by Coq against a + RustBelt-based model **[External]** (PLDI'24 paper); SAW's verification + of C and Rust implementations via Crucible symbolic execution + **[External]** (saw-script user manual; crux comparison doc); MIRAI's + path-sensitive, full-program abstract interpretation from package entry + points **[External]** (MIRAI README and Architecture doc). Different + limitations; none universal — but unsafe reasoning, whole-program + analysis, and machine-consumable verification are not absent from the + landscape. +- **Authority at the execution boundary.** Compile admitted Rust for a + Wasmtime/WASI environment with only approved imports: WASI is built on + capability-based security — no ambient authority, every resource access + through host-granted handles, deny-by-default at the runtime boundary + **[External]** (bytecodealliance/wasi.dev docs/security.md). Even unsafe + guest code does not thereby gain arbitrary host syscall authority. This + removes revision 2's "any crate can simply open anything" premise without + claiming to reproduce Hum's source-level effect system. +- **Supply-chain as admission decisions.** cargo-vet exposes machine- + readable output (`--output-format=json`) **[External]** + (mozilla/cargo-vet PR #97) — dependency accounting need not be + reconstructed manually. An audit is not a functional-correctness proof, + and the ledger must preserve that distinction. +- **The authoritative checker** is the one part nobody has built: + obligation identities, coverage, assumption records, the + bounded-vs-enforced distinction, refusal of missing or stale evidence. + That is an engineering gap — plausibly a one-to-two-year project for a + constrained profile — not a language barrier **[Inference]**. + +The question revision 2 could not answer: **which necessary part requires +different executable-language semantics rather than a compiler extension, +restrictions, contracts, or an execution boundary?** The record does not +identify that part. + +## Where Revision 2 Was Wrong + +**1. The ledger as artifact.** The practical criticism was fair: separate +verifier outputs do not automatically constitute a complete, trustworthy +program account, and no off-the-shelf cross-tool ledger was found. But "a +human currently assembles these facts" does not imply "a tool cannot +assemble and validate them": Creusot ships a compiler wrapper and driver +with machine-identifiable contract annotations; cargo-vet produces +structured dependency evidence **[External]**. The hard work is identifying +all applicable obligations and their semantic dependencies, not printing +one JSON file — and calling the emitter "the compiler" would not solve +that work for Hum either. There was also a logical error: showing each +half of the property separately bolt-on-able does not show their +conjunction is bolt-on-able; revision 2's "either half" test was stronger +than its argument required. **[Inference]** + +**2. Per-crate unsafe.** Correct about ordinary builds — a crate's lint +does not reach third-party dependencies, and build scripts are separately +compiled programs. But revision 2 misstated `forbid` as "un-overridable": +`--cap-lints` can lower even forbidden lints, and Cargo caps lints for +dependencies **[External]** (rustc lint-level docs; cargo book). Workspace +`[lints]` forbid never reaches third-party unsafe, full stop. The stronger +response is a trusted driver that checks the whole admitted closure, +controls lint capping and build inputs, and rejects new unapproved trust +dependencies — PL/Rust already demonstrates this architectural pattern: a +specialized Rust driver enforcing restrictions with a separate, documented +dependency-vetting boundary ("it is the administrator's responsibility to +properly vet external dependencies") **[External]** (plrust.io config-lints +docs). And the hardest requirement — arbitrary native dependencies without +assumptions — is one Hum does not meet either. **[Inference]** + +**3. FFI.** "FFI is the unverifiable floor" is false as stated. Verus is +not the only unsafe-capable tool: Kani explicitly verifies unsafe Rust +code (its team verified `CStr`'s raw-pointer code with unsafe harnesses) +**[External]**, and RefinedRust verifies safe and unsafe Rust with +proof-assistant-checked proofs **[External]**. Verus's `--no-cheating` +rejects `assume`/`admit`/`external_body`/`assume_specification` **in the +current crate only** — admitted specs in dependencies (e.g. vstd) sit +outside it **[External]** (verus-lang/verus#1499); Gale's 133 +`external_body` + 2 `assume_specification` is a report about Gale, not a +universal claim that real projects cannot pass. SAW shows cross-language +verification is possible with compatible memory models: a language +boundary is not intrinsically a proof boundary **[External]**. The deeper +correction cuts both ways: even an unverifiable implementation can satisfy +accountability if its assumptions, affected obligations, and permitted +effects are identified — but it cannot satisfy unconditional correctness +merely by receiving a label. **[Inference]** + +**4. Composition.** The warning was correct: a proof of `f` plus a bounded +proof of `g` does not automatically yield a program theorem. But different +trusted components are not themselves the obstacle — one can explicitly +trust their union. The real questions are whether the tools agree about +the program and property, whether assumptions are compatible, and whether +callers establish the conditions callees were verified under: a proof of +`g` under `n ≤ 16` supports a caller theorem only where the caller +establishes the bound; a ledger must track that implication, not +concatenate success reports. **[Inference]** Revision 2 misrepresented +Aeneas: its architecture describes compositional proofs in which callers +reuse proved function specifications — not requiring whole-program analysis +is not the same as being unable to represent a program-level account +**[External]** (aeneas architecture overview). The honest Aeneas +limitation: the account is split across three trust domains (Rust source → +translation → external prover); unsafe/unsupported code becomes opaque +declarations, each an unverified trust boundary; the translation's +symbolic-execution core was formalized at ICFP'22, but the implementation's +fidelity to that core is not machine-checked, and it functionalizes a +subset of safe Rust **[External]**. Hum's 0005 is a sensible authority +policy — external verifiers are evidence producers returning +`proved`/`refuted`/`unknown`/`unsupported`/`timeout` receipts +**[Requirement]** (0005-keep-verifiers-as-evidence-producers.md) — but not +the missing composition theorem: its linked boundary document calls itself +an architecture boundary, not an integration contract, and receipt import +is future work. + +**5. Capability.** The cap-std claims stand: it is not a sandbox for +untrusted Rust, and `open_ambient_dir` is not sandboxed **[External]** +(cap-std README). But revision 2 called the whole leg fictional, which +overreached: Cackle is an existing partial approach with acknowledged +holes — relevant to dependency API restrictions and compile-time +sandboxing, not a fictional leg **[External]**. And Wasmtime/WASI gives a +stronger host boundary than revision 2 considered: it does not make unsafe +Rust source semantics sound, and a module-level sandbox does not reproduce +Hum's per-task grant algebra — source analysis or finer +compartmentalization would still be required. Hum's legitimate advantage is +potentially a uniform, finer-grained authority discipline expressed in +ordinary interfaces. The unsupported leap was from that advantage to the +impossibility of an enforced Rust profile. The comparison must use the same +admitted features on both sides. **[Inference]** + +**6. Soundness gaps.** Recast as a coverage-and-trust inventory, not +disqualifiers. Architecture dependence (Creusot) is a scope condition, not +unsoundness, when the target is part of the theorem **[External]** +(Creusot limitations). Unsupported features are not soundness failures +when the checker rejects them or reports incomplete coverage. Flux's +"cannot distinguish logic errors from undefined behavior" is a diagnostic +distinction — the cited statement does not mean Flux silently accepts both +**[External]**. Unverified translations and solvers are trusted-base +issues that Hum's compiler and its future external-verifier integrations +face too. **[Inference]** + +**7. Kani bounds.** Machine-checked via unwinding assertions: an +insufficient bound fails the unwinding assertion and the proof is reported +unsuccessful — not silently accepted **[External]** (Kani paper GCD case +study; Rust std-verification paper; kani#889 reports such failures as +UNDETERMINED rather than misleading SUCCESS). The real distinction: a +harness assumption (`n ≤ 16`) restricts the theorem; an unwind parameter +controls loop expansion, and with passing unwinding assertions it is not +permission to ignore longer reachable executions **[External]**. Not every +stub is unchecked either: verified contracts and `stub_verified` reuse +verified abstractions rather than arbitrary replacements. The vacuity +warning is legitimate — contradictory assumptions make any proof +uninformative — but not Kani-peculiar. And 0020's quantitative bound is a +property of program execution, while a model-checking bound describes +verification scope or exploration: related but distinct fields, which 0020 +itself keeps separate **[Guarantee]**. + +## Hum's Own Trusted Base (Symmetric) + +Revision 2 said Hum trusting its Rust-written toolchain was "the same +position as Rust trusting rustc" — then counted every Rust internal +against the steelman while excluding Hum's own. The symmetry requirement is +decisive: if Hum may put file adapters, allocation machinery, and JIT +execution behind a fixed trusted implementation boundary, a Rust profile +may put an approved runtime or standard-library subset behind an +equivalent boundary. **[Inference]** + +Hum's guarantee, stated conditionally: + +> Assuming the compiler, runtime and named host primitives implement their +> specified semantics, every accepted source operation and profile-defined +> obligation has a recorded disposition. + +Hum's main crate keeps `#![deny(unsafe_code)]` **[Implemented]** (0017), +with exactly one reviewed, priced, scoped JIT exception — but the number of +unsafe blocks is a poor metric: one block can invoke a large backend, and +splitting or merging blocks changes nothing about assurance. Track trusted +contracts, reachable implementation dependencies, granted authority, and +assumption changes — not primarily exception count. Conversely, Hum cannot +move arbitrary behavior into a host primitive and thereby make its +assumptions disappear: the primitive's effects, relevant failure behavior, +and trusted contract must remain visible at the program boundary. +**[Inference]** + +## Which Hum Decisions Carry The Objective (Corrected) + +Revision 2 turned several requirements into stronger guarantees than their +sources support. Corrected: + +- **0015 — the check-treatment vocabulary [Requirement].** The four classes + govern runtime-check policy, not compiler evidence results: `proved` — + mechanically established for relevant build inputs; `boundary` — + enforced where authority or trust crosses a program boundary; `unproved` + — checked but not mechanically established; `external-trust` — depends + on data, code, or authority outside Hum's proof + (0015-adopt-classified-runtime-contract-policy.md). `boundary` is not + "bounded" in the loop-bound sense. The classifier is unimplemented — + "current Hum assigns none" — so the vocabulary exists without + assignment. +- **0016 — a narrow causal-error guarantee [Guarantee, scoped].** Known + fallible calls in currently executable expression positions never + propagate implicitly (0016-adopt-explicit-causal-typed-failure.md). + Explicitly outside the decision: first-class `Result`, checked variant + membership, exhaustiveness, recovery/catch, narrowing, exceptions, + unwind, ambient backtraces. A narrow, honest guarantee — not "every + failure path is a labeled, visible edge." +- **0017 — closed direct-call authority [Implemented].** The app declares + the maximum source authority; tasks declare transitive closure; callers + cover callees; unknown capability-like IDs fail closed. Source + declaration is never consent; sandbox-bypass authority (process launch, + FFI, unsafe, unrestricted import) is a separate severity tier. Main crate + `#![deny(unsafe_code)]` with one priced, scoped JIT exception. +- **0020 — bound claims separated [Guarantee].** Termination measures, + quantitative loop bounds, verification results, and completion claims are + distinct concepts that do not merge. +- **SPEC — controlled admission, not categorical refusal [Requirement].** + "Unsafe code is allowed only inside visible unsafe boundaries" + (SPEC:647) and "Compile-time code must be sandboxed by capabilities" + (SPEC:763) are stated requirements, phrased as such. `trusts:` names + explicitly unchecked assumptions. The macro/effects non-goals are design + commitments, not gates. This makes the enforced-Rust-profile comparison + more relevant, not less. +- **math_obligations.rs [Implemented].** Recognizes allocation-free claims + from `allocates:` and `cost:` sections and emits identified obligations + — explicitly labeled "not proof." That is more than parsing: an unproved + declaration can already be accounted for, even if no + allocation-freedom proof exists yet. +- **0014 §3 [Requirement].** Checked source relationships for returned and + stored views are a proposed requirement — the decision's status is still + explicitly proposed — with broad locks retained on stored/internal + references and general borrowing. The established local direct-field + alias slice is much narrower. +- **0005 [Requirement].** External verifiers are evidence producers, not + compiler authority; the receipt vocabulary + (`proved`/`refuted`/`unknown`/`unsupported`/`timeout`) is established. + Cross-backend composition is not. + +## Gaps That Currently Break It + +Today Hum does **not** deliver this objective. The record is a design +commitment; reading it as a status claim would be false. **[Inference]** + +- **0015's classifier is unimplemented.** No contract has been mechanically + classified. +- **0014's ownership debt.** Memory obligations are the largest + unaccounted region. +- **`allocates:`, `cost:`, `calls:`.** Allocation-free *claims* are + already accounted for as identified evidence records; allocation-freedom + proofs do not exist. `cost:` remains future-checked. +- **Higher-order blame is unsettled; effect polymorphism is pending** + (0015 consequences). Tasks-as-values cross the account's current edge. +- **Trust growth is the metric to watch** — trusted contracts, reachable + implementation dependencies, granted authority, assumption changes — + not primarily the exception count. + +## The Falsifier (Symmetric Operational Test) + +Adapted from the independent thesis review. It applies the same test to +both sides — anything less moves the goalposts **[Inference]**: + +1. **Fix the comparison.** Specify the same application subset, + obligation vocabulary, target, allowed host services, and + trusted-platform boundary for Hum and the Rust profile. +2. **Require an authoritative artifact.** For each accepted build, a + machine-checkable account must cover all profile-defined obligations, + expose transitive assumptions, distinguish proof scope from + enforcement, and bind to the actual build inputs and executable + artifact. +3. **Test enforcement adversarially.** Introduce an unaudited dependency, + hidden ambient access, build-generated code, a configuration-dependent + verification/execution mismatch, a stale receipt, an unsupported call, + and a contradictory assumption. Each must be rejected or produce the + explicitly permitted, visible disposition — not silently retain a + stronger claim. +4. **Evaluate maintenance against a declared policy.** Trust growth must + require authorization and have an explainable effect on downstream + claims. Zero unsafe is not necessary. + +An implementation satisfying that contract would defeat the design +objective's claim to need a new language, regardless of its branding or +verifier combination. + +**Internal falsifier.** A single accepted operation that bypasses the +supposed complete account is more decisive than an increased exception +count. Separately, an account dominated by broad assumptions may be +complete but practically unhelpful — completeness and usefulness need +different failure criteria. + +## A Comparative-Evidence Plan + +The language argument that survives the review is not exclusive ownership +of a ledger. A language does not need an assurance property that no +sufficiently powerful compiler extension could reproduce; it can justify +itself by making a valuable discipline **coherent, default, teachable, +and economical** — and that requires comparative implementation and +usability evidence. **[Inference]** + +- **Exactly-once linear resources.** Hum's ownership decision calls for + exactly-once resource protocols. Rust explicitly permits safe + `mem::forget` and does not guarantee destructor execution — so a genuine + linear-obligation guarantee would be stronger than Rust's ordinary + ownership guarantee (subject to carefully specified abort, divergence, + and failure behavior). But a restricted Rust profile could reject + forgetting or verify the protocol: the stronger case demonstrates the + *cost* of the encoding — invasive wrappers, restrictions that damage + ordinary library interoperability, difficult annotations, or trusted + implementations that Hum's native model avoids. +- **Stored and returned views (0014).** A promising candidate only after a + concrete example establishes what Hum accepts naturally, what ordinary + safe Rust cannot express directly, and what the Rust workaround costs. + 0014 currently commits to that work rather than proving its success. + +Programs 2 and 3 are chosen to produce this evidence (below). And the +consequence revision 2 drew does not follow: failing to establish +exclusivity does not establish that Hum's integrated language design has +no value — so "stop growing the checker" is removed as a consequence of +the thesis failing. + +## Consequence For Programs 2 And 3 + +Programs 2 and 3 are chosen to produce the comparative evidence above, not +to demo syntax **[Inference]**: + +- **Program 2: a config-file parser.** The `external-trust` boundary in + its most common real-world shape: untrusted input crosses a checked + boundary into internal handling. Tests 0016's typed failure across the + trust crossing and forces honesty from `allocates:` / `cost:` for + buffers. +- **Program 3: a small state machine with ownership transfer.** 0014's + closure discipline, 0015's check-treatment classes, and 0017's authority + boundary across state transitions — and, where it applies, the + linear-resource protocol case against the cost of Rust's encoding. + +Both should be instrumented against the friction ledger: where exactly +does the accountability demand bite the programmer? The try-rule question +stays downstream of wordfreq's ledger, not taste. + +## What Acceptance Commits Us To + +Accepting this record is not free **[Inference]**: + +- The 0015 classifier moves up in priority — vocabulary without assignment + is the half of the objective Hum does not have at all. +- Declared-only sections (`allocates:`, `cost:`, `calls:`) must either + become checked obligations or be explicitly labeled as unaccounted. +- Trust growth becomes the tracked budget: trusted contracts, reachable + implementation dependencies, granted authority, assumption changes — + reviewed like a budget. +- Programs 2 and 3 are chosen to produce the comparative evidence above. +- **The enforced-Rust-profile comparison must land before this record is + used to decide the language-versus-toolchain investment.** That + comparison is the missing half of the argument. + +## Sources + +Every **[External]** claim above is checkable at one of these primary +sources: + +**The enforced profile — build, supply chain, execution boundary** + +- Cackle (dependency API/`unsafe` ACLs; build-script, test, and rustc + sandboxing; documented circumvention limits): + https://github.com/cackle-rs/cackle/blob/HEAD/README.md and + https://github.com/cackle-rs/cackle/blob/HEAD/CONFIG.md +- cargo-vet machine-readable output (`--output-format=json`): + https://github.com/mozilla/cargo-vet/pull/97 +- WASI capability-based security (no ambient authority; host-granted + handles; deny-by-default at the runtime boundary): + https://github.com/bytecodealliance/wasi.dev/blob/HEAD/docs/security.md +- PL/Rust specialized-driver pattern ("the administrator's + responsibility to properly vet external dependencies"): + https://plrust.io/config-lints.html + +**Verifiers in the landscape** + +- RefinedRust (foundational verification of safe and unsafe Rust; + Coq-checked proofs against a RustBelt model; PLDI'24): + https://iris-project.org/pdfs/2024-pldi-refinedrust.pdf +- SAW (verification workbench; Crucible symbolic execution; MIR/Rust + backend): + https://github.com/galoisinc/saw-script/blob/HEAD/doc/saw-user-manual/overview.md + and https://github.com/galoisinc/crux/blob/HEAD/docs/comparison.rst +- MIRAI (path-sensitive, full-program abstract interpretation from + package entry points): + https://github.com/facebookexperimental/mirai/blob/HEAD/README.md and + https://github.com/facebookexperimental/mirai/blob/HEAD/documentation/Architecture.md +- Kani unwinding assertions (insufficient bound fails the proof; + UNDETERMINED reporting): https://arxiv.org/pdf/2607.01504, + https://arxiv.org/pdf/2606.17374v1, and + https://github.com/model-checking/kani/pull/889 +- Kani on unsafe Rust (`CStr` raw-pointer verification): + https://github.com/model-checking/kani-verifier-blog/blob/HEAD/_posts/2024-12-03-safety-of-cstr.md +- Verus `--no-cheating` (crate-scoped; current crate only; does not cover + dependency specs): https://github.com/verus-lang/verus/pull/1499 and + https://github.com/lasyaalluru/semi-persistent/blob/HEAD/containers-verus/doc/design/02-trust-boundary.md +- Aeneas (compositional proofs in the target prover; subset of safe Rust; + opaque declarations as trust boundaries): + https://github.com/aeneasverif/aeneas/blob/HEAD/documentation/aeneas-overview.md + and https://github.com/aeneasverif/aeneas/blob/HEAD/README.md + +**Verus** + +- Verus paper (SMT verification, ghost code, linear ghost permissions, + unsafe reasoning): https://arxiv.org/abs/2303.05491 +- Anvil verified Kubernetes controllers: + https://github.com/anvil-verifier/anvil +- `external_body` ("wrong specifications can subvert Verus's guarantees"): + https://github.com/verus-lang/verus/blob/HEAD/source/docs/guide/src/calling-unverified-from-verified.md +- `assume_specification` (unchecked, CAUTION banner): + https://github.com/verus-lang/verus/blob/HEAD/source/docs/guide/src/reference-assume-specification.md +- Gale trust inventory (133 `external_body` + 2 `assume_specification`, + a report about Gale — not a universal claim): + https://github.com/pulseengine/gale/blob/HEAD/docs/research/verus-quickstart.md + and https://github.com/pulseengine/gale/blob/HEAD/docs/safety/verification-honesty.md + +**Flux** + +- PLDI 2023 paper (refinement types for Rust): + https://dl.acm.org/doi/10.1145/3591283 and + http://arxiv.org/pdf/2207.04034 +- Tool summary (checks, `trusted`/`ignore`, unsafe limits, + quantifier-free ceiling): + https://github.com/model-checking/verify-rust-std/blob/HEAD/doc/src/tools/flux.md +- `#[flux_rs::trusted]` ("simply *trust* that the specification is + correct"): + https://github.com/flux-rs/flux/blob/HEAD/book/src/guide/specifications.md + +**Creusot** + +- "A deductive verifier for (safe) Rust code": + https://github.com/creusot-rs/creusot/blob/HEAD/ARCHITECTURE.md +- Limitations (architecture-specific proofs): + https://github.com/creusot-rs/creusot/blob/HEAD/guide/src/limitations.md +- ICFEM'22 paper (RustHornBelt mechanization gap): + https://jhjourdan.mketjh.fr/pdf/denis2022creusot.pdf +- Community std-verification lessons (incl. the Flux pointer-write + limitation at §2.2): https://arxiv.org/pdf/2510.01072 + +**Kani** + +- Soundness ("What Kani Does NOT Check"; CBMC caveats): + https://github.com/model-checking/kani/blob/HEAD/docs/src/soundness.md +- RFC 0004 (unbounded loops unrolled to a user-specified threshold): + https://github.com/model-checking/kani/blob/HEAD/rfc/src/rfcs/0004-loop-contract-synthesis.md +- Issue #3679 (foreign function unsupported in that verification + setting; aws-lc-sys): + https://github.com/model-checking/kani/issues/3679 +- Stubbing (`#[kani::stub]`; verified contracts and `stub_verified` + reuse verified abstractions): + https://github.com/model-checking/kani/blob/HEAD/docs/src/reference/experimental/stubbing.md +- Vacuity guidance (`kani::cover!`): + https://github.com/strawgate/memagent/blob/HEAD/dev-docs/references/kani-verification.md + +**Lints, policy, capabilities** + +- rustc lint levels (`--cap-lints` can lower even forbidden lints): + https://doc.rust-lang.org/nightly/rustc/lints/levels.html +- Cargo `[lints]` (applies to the current package only; dependencies + capped): + https://github.com/rust-lang/cargo/blob/HEAD/doc/book/src/reference/manifest.md +- rustc `unsafe_code` lint (catches `unsafe`, `no_mangle`, + `export_name`, `link_section`): + https://doc.rust-lang.org/stable/nightly-rustc/rustc_lint/builtin/static.UNSAFE_CODE.html +- rust-lang 2024-H2 std-verification goal (Creusot's self-description as a + safe-Rust verifier): + https://github.com/rust-lang/goals/blob/HEAD/src/2024h2/std-verification.md +- aegaeon unsafe-code policy (per-crate geiger gate; deps scan for + visibility only; build scripts are separate crates): + https://github.com/codetakt/aegaeon/blob/HEAD/docs/policies/unsafe-code-policy.md +- cap-std README (`open_ambient_dir` not sandboxed; "not a sandbox"): + https://github.com/bytecodealliance/cap-std/blob/HEAD/README.md +- Creusot project trust inventory ("What remains trusted"): + https://github.com/crumplecup/elicitation/blob/HEAD/CREUSOT_TRACKING.md + +## Ruling + +Accepted as a scoped design objective and research plan. BDFL ruling +2026-09-23 (revision 3): revision 3 is the rewrite the BDFL asked for after +rejecting revision 2, so it is not "rejected" — revision 2's rejection is +history. Revision 2 stands rejected as written (BDFL ruling 2026-09-22): +0026 was NOT accepted as the justification for a non-bolt-on property. The +non-bolt-on exclusivity claim stays withdrawn. + +**Review history.** (1) Pre-issuance execution review of revision 2: +Claude, 2026-09-22 — with disclosure that the thesis wording is Claude's, +so that review covers execution accuracy only, not the truth of the +thesis. (2) Independent thesis review: ChatGPT Pro, full text received via +Ocean 2026-09-22 — a document/source review with external primary-source +spot checks (not an execution of any test suite). Verdict: does not hold +as written. (3) Execution re-check of revision 3: Claude, 2026-09-22 — the +exclusivity claim is gone, every tool the review named is in the steelman +(Cackle, RefinedRust, SAW, MIRAI, Wasmtime/WASI), the forbid/cap-lints +correction is in, evidence labels are split into Requirement / Implemented +/ Guarantee throughout, the falsifier is the symmetric one, "stop growing +the checker" is explicitly removed, the comparative plan leads with linear +resources versus `mem::forget`, and the review history is recorded +honestly, including Claude's conflict of interest. +Revision 3 addresses the independent review's findings: the stronger +enforced-profile steelman; the ledger-artifact correction; the per-crate +forbid correction; the FFI corrections; composition and the corrected +Aeneas account; the capability correction; the coverage-and-trust +inventory; the Kani-bounds correction; the obligation universe and +evidence model with the corrected 0015 mapping; the symmetric trusted base +with the conditional guarantee; every overstated claim re-split into +Requirement / Implemented / Guarantee; the symmetric operational +falsifier; the removed "stop growing the checker" consequence; and the +comparative-evidence plan. The enforced-Rust-profile comparison gates the +language-versus-toolchain INVESTMENT decision, not this record — this +record is what commissions that comparison.