Eunomia OS - Verus rewrite

This is the fourth in a series of blog posts about my experimental operating system, Eunomia. Previous post is at Eunomia OS - more verification, the first at Eunomia OS - first day.

Planning

The idea was to add the first proper formal verification, by deductive reasoning using Verus. The previous methods included only model checking and fuzzing.

As always, first a plan. It turned out that it was best to just completely scrap Kani and replace it with Verus. Another notable thing about the plan was that it included a major change of the existing code. The cspace tree, which used raw *mut CapSlot to track parents, children, and siblings, was to be rewritten to use typed indices in a eventually.

Implementation

Phase 1 went rather smoothly, but Phase 2 turned out to be harder. It went through multiple attempts.

The first roadblock was at the #53. Opus was trying to prove that insertion into the capability derivation tree preserves acyclicity, but gave up:

I've hit the genuine hard core: the acyclicity witness construction for insert_child is blocked because my structural cdt_wf is too weak to guarantee "a leaf has no children" (it doesn't pin parent↔child-list consistency — that needs reachability reasoning). Rather than chase a deep cdtwf strengthening that risks the whole session, let me pivot to what's cleanly provable: *termination via using the acyclicity witness (not constructing it). Let me restore cspace.rs to the clean #53 state and re-apply just the acyclicity predicates plus a fully-proven descend_to_leaf + revoke termination.

The result: 3verus-rewritecloseout-detail.md. To make sure the "fresh-eyes re-derivation" is followed, I temporarily deleted the docs before 9b, but copied that part, and pasted after:

>Hello! Please conduct an audit of this repository, precise instructions below. I've temporarily removed all of the documentation irrelevant for this task to reduce distractions. Feel free to use ultracode workflows to organise the work. Instructions:

Note that Opus understood what "fresh eyes" means. I don't want to know what would happen if I was a science fiction character talking to a robot!

Opus then produced this workflow:

export const meta = {
  name: 'verus-spec-rev2-audit',
  description: 'Fresh-eyes audit: does Verus-verified code implement spec rev2? Drift ledger.',
  phases: [
    { title: 'Audit', detail: '8 section-auditors derive spec property cold, then read code' },
    { title: 'Verify', detail: 'adversarial skeptic per candidate drift' },
    { title: 'Synthesize', detail: 'merge confirmed drifts into the drift ledger' },
  ],
}

const REPO = '~/repo/eunomiaos'
const SPEC = `${REPO}/doc/spec/2_spec_rev2.md`

// Shared discipline preamble handed to every auditor and verifier.
const DISCIPLINE = `
You are a Verus-verification auditor on the Eunomia OS microkernel. The goal is to
confirm — or refute — that the *verified code* faithfully implements the *design spec*
at ${SPEC}, judged ONLY against the spec text and the actual code.

HARD RULES (the integrity of this audit depends on them):
- Authority = the spec file (${SPEC}) and the Rust source. NOTHING ELSE.
- Do NOT read or trust: doc/results/* (findings docs), doc/plans/* (the plan's
  obligation tables), or the CLAUDE.md narrative. The accumulated justification prose
  is exactly what this audit must ignore — a proof can be green against a DRIFTED
  obligation, and the chain of justifications rationalizes the drift.
- Code COMMENTS (including ones citing "plan §6e", "doc 23", "doc 55") are CLAIMS TO
  VERIFY, not authority. Read the actual 'spec fn' model + 'requires' + 'ensures' and
  judge for yourself. A comment asserting a property is not the same as an 'ensures'
  proving it.
- Verus vocabulary: 'spec fn' = the mathematical model; 'requires' = precondition;
  'ensures' = the proven postcondition; 'open/closed/uninterp spec fn' (uninterp = an
  UNINTERPRETED function — an abstraction seam where nothing is proven about its body);
  '*_wf' predicates = well-formedness invariants. The proven guarantee of a function is
  EXACTLY its 'ensures' under its 'requires' — nothing the comments add.

METHOD (follow in order — do not look at 'ensures' before step 2):
1. Read your assigned spec section(s) COLD from ${SPEC}.
2. In YOUR OWN WORDS, write the property the implementation OUGHT to guarantee, derived
   from the spec text ALONE, BEFORE opening any code. This is 'derived_properties'.
3. Open the verified code. Read the 'spec fn' model, 'requires', 'ensures'. Ask:
   (a) Does the proven postcondition MATCH the spec-derived property, or a convenient
       WEAKENING of it?
   (b) Is the 'spec fn' model (cdt_wf, chan_wf, the FIFO Seq, pt_wf, run_len, etc.) a
       faithful encoding of the spec's intent, or shaped to what was provable?
   (c) Does a 'requires' EXCLUDE inputs the spec admits? If so, is the excluded case
       handled elsewhere, or genuinely impossible? (You must locate where, or flag it.)
4. Record every gap as a DRIFT, classified:
   D1 = model weaker than spec (the 'ensures' proves LESS than the spec promises).
   D2 = precondition hides a case (a 'requires' excludes inputs the spec admits — e.g.
        an is_homed guard, a gen_a != gen_b assumption; you MUST say where the excluded
        case is handled, or that it is unhandled/impossible).
   D3 = spec ambiguity (spec underspecified, code picked a reading — record the reading).
   D4 = code correct, spec stale (spec text lags the implemented design).
   Where the code FAITHFULLY matches the spec, say so explicitly (is_drift=false) — a
   confirmed match is a real audit result, not a non-finding.

Be concrete: every drift cites a spec anchor (section + what it says) and a code anchor
(file:line + the exact 'ensures'/'spec fn'/'requires' clause). Severity reflects whether
a real safety/security property of the spec is unproven, not stylistic gaps. Use Read,
Grep, Bash(grep/rg) freely. The cargo target dir is at ${REPO}/target.
`

const FINDER_SCHEMA = {
  type: 'object',
  additionalProperties: false,
  required: ['unit', 'derived_properties', 'drifts', 'faithful_matches', 'summary'],
  properties: {
    unit: { type: 'string' },
    derived_properties: {
      type: 'array',
      description: 'Spec-derived ought-to-guarantee properties, written BEFORE reading ensures.',
      items: {
        type: 'object',
        additionalProperties: false,
        required: ['property', 'spec_basis'],
        properties: {
          property: { type: 'string' },
          spec_basis: { type: 'string', description: 'spec section + quoted phrase' },
        },
      },
    },
    drifts: {
      type: 'array',
      items: {
        type: 'object',
        additionalProperties: false,
        required: ['title', 'spec_anchor', 'code_anchor', 'spec_says', 'code_proves',
                   'classification', 'evidence', 'severity', 'proposed_disposition'],
        properties: {
          title: { type: 'string' },
          spec_anchor: { type: 'string', description: 'spec section + quoted phrase' },
          code_anchor: { type: 'string', description: 'file:line + the exact clause' },
          spec_says: { type: 'string' },
          code_proves: { type: 'string', description: 'the actual ensures/model, in plain terms' },
          classification: { type: 'string', enum: ['D1', 'D2', 'D3', 'D4'] },
          evidence: { type: 'string', description: 'why this is a gap; for D2, where the excluded case is/ isn’t handled' },
          severity: { type: 'string', enum: ['high', 'medium', 'low'] },
          proposed_disposition: { type: 'string', enum: ['fix-now', 'follow-on', 'accepted-documented'] },
        },
      },
    },
    faithful_matches: {
      type: 'array',
      description: 'Properties where code FAITHFULLY matches spec (explicit non-drifts worth recording).',
      items: {
        type: 'object',
        additionalProperties: false,
        required: ['property', 'code_anchor'],
        properties: {
          property: { type: 'string' },
          code_anchor: { type: 'string' },
        },
      },
    },
    summary: { type: 'string' },
  },
}

const VERIFY_SCHEMA = {
  type: 'object',
  additionalProperties: false,
  required: ['verdict', 'final_classification', 'reasoning', 'excluded_case_resolution',
             'final_severity', 'final_disposition', 'confidence'],
  properties: {
    verdict: { type: 'string', enum: ['confirmed', 'refuted', 'reclassified'] },
    final_classification: { type: 'string', enum: ['D1', 'D2', 'D3', 'D4', 'not-a-drift'] },
    reasoning: { type: 'string', description: 'Independent re-derivation. Quote the actual ensures/requires you read.' },
    excluded_case_resolution: { type: 'string', description: 'For D2: where IS the excluded case handled (file:line) or is it genuinely impossible? "n/a" otherwise.' },
    final_severity: { type: 'string', enum: ['high', 'medium', 'low'] },
    final_disposition: { type: 'string', enum: ['fix-now', 'follow-on', 'accepted-documented', 'none'] },
    confidence: { type: 'string', enum: ['high', 'medium', 'low'] },
  },
}

// ---- The 8 audit units. Each names spec sections + precise code anchors + watch-list hooks.
const UNITS = [
  {
    key: 'A-revocation-cdt',
    label: 'A:§2.2 revocation+CDT',
    prompt: `${DISCIPLINE}

YOUR UNIT: §2.2 "Revocation — hybrid model" + the §3.4 consequence that queue slots are
CDT-visible + the §6 row-(b) revocation invariant.

Spec to read cold: §2.2 (kernel-cap CDT: "revoke(cap) eagerly deletes all descendants",
"revocation sees through queues — the guarantee is unconditional, with no 'except messages
in flight' caveat"; retype soundness depends on revoke proving exclusivity), §3.4 ("Queue
slots are real, CDT-visible capability slots ... Revocation therefore finds and deletes
in-flight caps like any other descendants — no special case in the revoke logic, no caveat
in its specification"), §6 table row (b) ("revocation model includes channel queue slots,
so 'revoke destroys all descendants' is checked unconditionally, in-flight caps included").

Verified code: kcore/src/cspace.rs. Key anchors:
  - pub fn revoke (~line 9291): read its full 'requires' and 'ensures'. Note the ensures
    has TWO parts — (i) final.slot.first_child is None (descendants gone) and (ii)
    !is_empty_cap(final.slot.cap) (the revoked cap SURVIVES). Which part, if any, is gated
    by the precondition '!is_homed(old(store), slot)'?
  - is_homed (~3593), lemma_is_homed_stable (~3648).
  - The CDT well-formedness model: grep for 'cspace_wf', 'cdt_wf', 'first_child',
    'parent', and how "no direct children" relates to "no descendants" (is there a
    transitivity/reachability lemma, or does wf give it structurally?).
  - How are in-flight (queued) caps modeled as CDT nodes? Grep channel.rs for queue-slot
    ownership and confirm revoke's descendant walk actually reaches them (or only could in
    principle). Does any 'ensures' state that revoke deletes caps queued in a channel?

WATCH-LIST (judge independently, don't assume drift): the spec's "revoke destroys all
descendants" — does it ADMIT the seL4-zombie self-empty case (revoking a cspace-resident
slot whose subtree holds the cspace's last live cap, so the cap self-empties)? The code
makes root-SURVIVAL conditional on !is_homed. Decide precisely:
  - Is the DESCENDANT-DESTRUCTION clause unconditional (spec's actual promise met)?
  - Is root-survival a STRONGER property the spec never explicitly promised (so gating it
    is fine), or does the spec implicitly promise the revoked cap survives?
  - Does '!is_homed' exclude any input where the spec WOULD demand descendant destruction
    but the code refuses? (i.e., is the precondition only narrowing the survival claim, or
    also narrowing which revokes are admitted at all?)
  - Crucial: is the "revoke sees through queues, unconditional, no caveat" guarantee
    actually PROVEN by an ensures, or only asserted by comments? If the queue-reaching is
    not in any ensures (only structurally implied by the descendant walk + wf), record the
    gap and its class.`,
  },
  {
    key: 'B-attenuation',
    label: 'B:§2.3 attenuation/derivation',
    prompt: `${DISCIPLINE}

YOUR UNIT: §2.3 "Attenuation and derivation lattice" — the monotonicity invariant.

Spec to read cold: §2.3 ("All derivations are monotone: authority can only shrink, never
grow"), the derivation-lattice table (untyped: sub-range page-aligned + rights mask;
channel/thread/cspace: rights mask only), thread rights bits + the §5.4 max-controlled-
priority ceiling ("attenuates the same monotone way"), the headline that "what can this
process touch?" is answerable by inspecting the cspace.

Verified code: kcore/src/cspace.rs. Find the operations that DERIVE/COPY/MINT caps (grep
for 'fn copy', 'fn mint', 'fn derive', 'rights', 'mask', 'attenuat', 'monoton'). For each:
  - What does the 'ensures' prove about the child's rights vs the parent's? Is monotonicity
    (child.rights ⊆ parent.rights) an actual proven postcondition, or only an unproven
    convention?
  - Untyped sub-range: is the page-aligned sub-range + rights-mask derivation proven to
    stay within the parent's range? (grep untyped.rs too if derivation lives there.)
  - Is there a 'spec fn' modelling "authority of a cap" against which monotonicity is
    stated, or is monotonicity only stated structurally per-field?
  - The §5.4 priority ceiling: is it on the cap and attenuated monotonically? grep
    thread.rs/cspace.rs for 'priority', 'mcp', 'ceiling'.

Judge: does the code actually PROVE the §2.3 monotonicity invariant for every derivation
the table lists, or is monotonicity asserted in prose while only some ops carry an ensures?
If derivation/mint is not verified at all (e.g. left to a non-Verus layer), that itself is
a finding about §2.3's verification claim — record it (likely D4 or a coverage gap).`,
  },
  {
    key: 'C-memory',
    label: 'C:§2.5 untyped+aspace+DMA',
    prompt: `${DISCIPLINE}

YOUR UNIT: §2.5 "Memory: frames, mappings, and DMA" + §3.1 bulk-window grant direction.

Spec to read cold: §2.5 — "retyping untyped memory is only sound if the kernel can
establish that no outstanding caps reference the region, and revoke is how exclusivity is
proven"; "pool-at-creation ... returns NEED_MEMORY when the pool is exhausted"; "Mapping
state lives in the frame cap: one mapping per cap copy, and deleting or revoking the cap
unmaps it"; DMA "phys-read rights bit on frame caps gates frame_paddr(cap)".

Verified code:
  - kcore/src/untyped.rs: retype_check (~150), carve / carve_place (~299/372), retype_install
    (~474), the watermark-reset proving exclusivity (~695, reset_slot ~668). Read the
    'ensures'. Does retype PROVE no-outstanding-caps / exclusivity over the carved region
    before retype, or assume it via a precondition? Is the carve arithmetic overflow-safe
    (the spec's "checked arithmetic" theme)? Is the exclusivity the spec demands actually an
    ensures, or only the watermark mechanics?
  - kcore/src/aspace.rs: pt_wf (~451), pt_wf_leveled (~471), pt_lookup (~355), map_in /
    walk_alloc, NEED_MEMORY/pool exhaustion. Is "mapping lives in the cap, revoking unmaps"
    actually modelled+proven, or is the proof only about page-table structural wf
    (pt_wf preserved, pt_lookup unchanged for unrelated va)? Is pool-at-creation's
    NEED_MEMORY path proven not to allocate kernel memory? Does map prove the leaf PTE
    encodes the requested perms (spec_pte_encode)?
  - dma-pool/: grep for 'phys', 'paddr', 'frame_paddr', and how phys-read is gated. Is the
    "PAs only visible here" boundary enforced in code, and is any of it Verus-verified?

Judge each spec promise against the actual ensures. The big one: is RETYPE EXCLUSIVITY
(the safety linchpin the spec calls out) a proven postcondition, or assumed?`,
  },
  {
    key: 'D-channels',
    label: 'D:§3.1-3.4 channels',
    prompt: `${DISCIPLINE}

YOUR UNIT: §3.1–§3.4 IPC channels — message format, send/recv semantics, FIFO, backpressure,
and capability move semantics.

Spec to read cold: §3.3 ("send is non-blocking, returns FULL when full; messages are never
dropped"; FIFO per channel; "On receive, transferred caps are installed into the receiver's
cspace; if the receiver lacks free slots, the receive fails and the message stays queued";
peer-closed / teardown-always-signals), §3.4 move semantics ("At every instant a capability
has exactly one owner — sender, queue slot, or receiver, never two"; "Receivers must tolerate
null cap slots"; "Channel destruction destroys queued caps"; "At most 4 caps per message").

Verified code: kcore/src/channel.rs. Anchors:
  - chan_wf and ring_fifo (the FIFO model as a Seq). Is ring_fifo a faithful FIFO encoding?
  - pub fn send (~651): ensures show the sending ring grows by Seq::push, the other ring
    unchanged, chan_wf preserved. Is FULL handled (the count<=depth guard)? Is "messages
    never dropped" reflected (no path silently drops)?
  - pub fn recv (~1011): ensures show receiving ring loses head (drop_first). CRITICAL:
    does recv prove the head message's CAPS are installed into the receiver's cspace? Does
    it model/handle the "receiver lacks free slots ⇒ receive fails, message STAYS queued"
    case (spec §3.3)? Or does the ensures only cover the dequeue and skip the cap-install /
    no-free-slot semantics?
  - MOVE SEMANTICS: is "exactly one owner at every instant" actually captured? When a cap
    is sent, does an ensures show it left the sender's slot AND occupies the queue slot
    (conservation), or only that the ring grew? Does recv prove conservation into the
    receiver? If conservation/no-duplication is only structural, say so.
  - Channel destroy: grep for destroy/teardown — does it prove queued caps are destroyed
    (CDT cleanup) and peer-closed fires? Tie to unit A's queue-CDT-visibility.

For each spec promise, state whether the ensures proves it or weakens it.`,
  },
  {
    key: 'E-notifications-timers',
    label: 'E:§3.6 notif+timers',
    prompt: `${DISCIPLINE}

YOUR UNIT: §3.6 "Event multiplexing: notifications now" + the timer object (§2.6, §3.6, §4.4).

Spec to read cold: §3.6 — "notification object — a single machine word of signal bits plus a
waiter queue. Signalers OR bits in; a waiter receives the accumulated word, which clears";
binding slots (on-readable/writable/peer-closed; IRQ; timer; thread) each a (notif cap, bit)
pair; "zero allocation on any event path" / "event delivery never allocates"; the lost-wakeup
discipline. §2.6/§4.4: timer object programs a deadline that signals a bound notification.

Verified code:
  - kcore/src/notification.rs: signal (~67), wait (~335), signal_wakes (~48), waiter_seq
    (the FIFO Seq model). Read ensures. Does signal prove bits are OR'd in and the head
    waiter dequeued (waiter_seq.drop_first)? Does wait prove the accumulated word is
    returned-and-cleared, and the waiter enqueued (waiter_seq.push)? Is the FIFO wake order
    (waiter_seq) a faithful model of "waiter queue"? Is the "word clears on receive"
    semantics actually in an ensures?
  - kcore/src/timer.rs: arm / disarm / expire (grep 'fn arm', 'fn disarm', 'fn fire',
    'fn check_expired', 'deadline'). Does the code prove arming binds a deadline to a
    notification and firing signals that notification's bit? Or is the timer->notif coupling
    only partially modelled?
  - NO-ALLOC claim: is "event delivery never allocates" reflected anywhere as a property
    (preallocated slots/records), or is it an architectural claim with no proof obligation?
    Record what is and isn't captured.

WATCH-LIST: the refcount_sound 'system clause' for notification 'wait' and timer 'arm/disarm'
is reportedly a per-op follow-on. Inspect: do wait / arm / disarm carry the conditional
'cspace::refcount_sound(old) ==> refcount_sound(final)' (and any EXTRA guards), or do they
establish it unconditionally? Note exactly which ops carry it conditionally vs not — this
feeds the cross-cutting refcount audit.`,
  },
  {
    key: 'F-threads',
    label: 'F:§5.1/§5.3 threads',
    prompt: `${DISCIPLINE}

YOUR UNIT: §5.1 startup/thread-as-unit-of-report + §5.3 faults.

Spec to read cold: §5.1 — "the thread is the unit of report"; each TCB carries on-exit and
on-fault binding slots (notif cap, bit), CDT-visible; a preallocated terminal report record
"running | exited(status) | faulted(cause, faulting address)"; "at most one terminal report
per thread (suspend-on-fault means no second fault)"; thread_exit(status) "recorded by the
kernel so a child can neither lie about nor forget its own death"; read_report; "a child
cannot silence or forge its own death notice". §5.3 — "A faulting thread is suspended, not
destroyed"; one record, two bits, one read_report; suspend-not-destroy.

Verified code: kcore/src/thread.rs. Anchors:
  - report_terminal (~144): ensures. Does it prove Running -> Exited|Faulted happens AT MOST
    ONCE and terminal states are ABSORBING (ReportMonotone)? Is "no second fault / at most
    one terminal report" an actual proven invariant, or a comment? Quote the monotonicity
    ensures.
  - bind (~224): ensures. Are the on-exit/on-fault slots configured only by the cap holder,
    and CDT-visible (so revoke sees through them)? Is the binding refcount accounted (ties
    to refcount_sound — does bind carry the conditional clause)?
  - thread_exit / fault path / read_report: grep. Does the model capture "status persists in
    TCB until parent reaps" and "faulting thread suspended not destroyed"?
  - Report record preallocation (no-alloc on death path): is the at-most-one-report bound
    what makes it preallocated-safe, and is that proven?

Judge: is the §5.1 "at most one terminal report, absorbing" guarantee proven (D-grade if
weaker)? Is the §5.3 suspend-not-destroy reflected (faulted state set, thread not removed)?
Note whether thread::bind carries refcount_sound conditionally (feeds cross-cutting unit H).`,
  },
  {
    key: 'G-storage',
    label: 'G:§4 commit/recovery',
    prompt: `${DISCIPLINE}

YOUR UNIT: §4 storage — the commit protocol, crash recovery, on-disk geometry validation,
and canonical-tree faithfulness (the Verus-verified parts of cas).

Spec to read cold: §4.2 (two superblock slots A/B; generation-checksummed A/B flip preceded
by fsync is "the single atomicity mechanism"; index commitment rules: self-reference padding,
the DEFERRED-REUSE invariant "no extent freed by commit N may be reused until N's barrier-2
has landed", no-wedging/non-tail-only placement), §4.3 (commit: barrier-1 fsync chunks/index,
build superblock gen+1 + WAL head advanced past the contiguous prefix of flushed records,
write to the OLDER slot, barrier-2 fsync; nothing freed on write path), §4.5 (crash recovery:
take higher-generation checksum-valid survivor; MOUNT VALIDATES EVERY GEOMETRY FIELD against
device length with checked arithmetic at a single chokepoint after checksum; replay WAL from
recorded head; discard checksum-failing tail; "recovery is TOTAL over arbitrary device
contents — never a panic, never unbounded allocation, never a read past device end"), §4.8
integrity (single-fetch, hash-what-you-stored).

Verified code:
  - cas/src/store.rs: mount (~957), commit (~1561), replay_bound (~651), run_len (~595),
    content_ok_spec (~583 — note: 'uninterp spec fn', an ABSTRACTION SEAM), frame_at (~492),
    laid_out (~764), lemma_run_len_covers, lemma_gap_freedom (~843), live_slot/commit_target.
  - cas/src/disk.rs: superblock encode/decode + geometry validation. grep 'spec_', 'checked',
    'geometry', 'validate', 'device_len', 'chunk_tail'.
  - cas/src/prolly.rs, cas/src/tree.rs: canonical / history-independent tree shape (§4.1, §4.9).

Derive the §4.5 recovery property: "recovered state = committed roots + replay of all WAL
records not covered by the committed head" (also the §6 row-(a) TLA+ invariant). Then check
what the Verus proof ACTUALLY establishes:
  - replay_bound ensures: r.end_off <= wal.len() (totality/in-bounds), r.count ==
    run_len(...) (maximal-run arithmetic), termination. Is the per-record ACCEPTANCE
    predicate 'content_ok_spec' UNINTERPRETED? If so, the proof is the STRUCTURAL/ARITHMETIC
    half only — content-coverage (that replayed records reconstruct the right state) is NOT
    mechanized here. Confirm precisely and classify.
  - mount geometry validation: is every superblock field validated against device length
    with checked arithmetic at one chokepoint (the §4.5 totality promise)? Is "total over
    arbitrary bytes — no panic / no unbounded alloc / no read past end" actually proven
    (e.g. bounded by input length, checked casts), or only tested by fuzzing?
  - commit: does any ensures capture the A/B-flip-to-older-slot + barrier ordering, or is
    commit's atomicity left entirely to TLA+? Is the deferred-reuse invariant present in
    code at all, or purely a TLA+/prose obligation?

WATCH-LIST: the phase-8 commit-recovery proof is reportedly the STRUCTURAL/ARITHMETIC half
only, with content-coverage left to TLA+. Decide whether the spec §6 row-(a) ("recovered
state = committed roots + replay") reads as FULLY MECHANIZED when in fact half is TLA+-only.
Note: spec §6 itself assigns the commit/recovery protocol to TLA+ (not to mechanized Verus)
— factor that into your classification (is the split spec-consistent, or does some artifact
overclaim mechanization?).`,
  },
  {
    key: 'H-crosscutting',
    label: 'H:refcount_sound + §6',
    prompt: `${DISCIPLINE}

YOUR UNIT (cross-cutting): (1) the refcount_sound "system invariant" globality question, and
(2) the §6 verification-strategy spec-vs-reality reconciliation.

PART 1 — refcount_sound. The spec never names "refcount_sound", but §2.2 makes refcount/
exclusivity the linchpin of retype soundness: "retyping untyped memory is only sound if the
kernel can establish that no outstanding caps reference the region". Read:
  - kcore/src/cspace.rs: refcount_sound (~3337: forall live obj, refs[o] == obj_census(o)),
    census_dom_complete (~3352), census_delta_frozen (~3377), obj_census (the census terms:
    slot_refs + binding + waiter + armed_timer + frame_map + thread_hold).
  - Then survey EVERY public mutating op across channel.rs, notification.rs, timer.rs,
    thread.rs, untyped.rs for how it treats refcount_sound. grep -n 'refcount_sound' across
    kcore/src. Classify each op as:
      (a) UNCONDITIONAL preservation (ensures: refcount_sound(final) outright),
      (b) CONDITIONAL preservation (ensures: refcount_sound(old) ==> refcount_sound(final)),
      (c) CONDITIONAL WITH EXTRA GUARD (e.g. channel bind: '(chan_view.dom().finite() &&
          refcount_sound(old)) ==> refcount_sound(final)'),
      (d) does NOT mention refcount_sound (silent — may break the chain).
  - The KEY question: is refcount_sound established as a SYSTEM-WIDE INVARIANT (some entry
    point/initial state establishes it, and a CLOSED SET of ops preserve it, so it always
    holds), or is it only a per-op conditional 'if it held, it still holds' with NO proof
    that it ever holds, and/or with ops in class (d) that could silently break it? The
    watch-list flags notification 'wait', timer 'arm'/'disarm', channel 'send'/'recv',
    'thread::bind', 'retype_install' as recorded per-op follow-ons — verify each, and decide:
    is "refcount soundness" CLAIMED more globally (e.g. in comments calling it a "system
    invariant per plan §6f") than the ensures actually PROVE? Note where the only thing
    binding the conditional clauses into a real invariant would be an unproven assumption
    that some caller chain always starts from a sound state.

PART 2 — §6 verification strategy. Read spec §6 cold (the tiered table). It says: Verus is
DEFERRED (struck through), Kani is the mechanized tier for kcore, TLA+ owns the commit/
recovery and cap-revocation PROTOCOL models. Now observe reality: grep -rl 'verus!' kcore/src
and cas/src — the kernel core IS Verus-verified (verus! macros everywhere), and there is a
kcore crate exactly as §6's deferred-Verus note describes the "later port shape". Decide:
  - Is spec §6 STALE (D4): it says Verus deferred / Kani is the tier, but the implementation
    is Verus-verified? Record the exact stale text.
  - Does any spec text or in-code contract OVERCLAIM what is mechanized (e.g. presenting the
    commit/recovery proof as fully Verus-mechanized when §6 assigns it to TLA+ and the Verus
    proof is the structural half only — coordinate with unit G's finding)?
  - Is there a coverage MISMATCH: §6 lists Kani harnesses (cspace/CDT, untyped, channels,
    notifications, thread reports, page-table walker, syscall decode, host chokepoints) —
    does that list still describe the actual verification, or has it been superseded by Verus?

Output drifts for Part 1 (likely D1/D3 about over-claimed globality) and Part 2 (likely D4
spec-stale on §6). Be precise about what the ensures DO prove so the disposition is fair.`,
  },
]

phase('Audit')
log(`Auditing ${UNITS.length} spec↔code units against ${SPEC} (fresh-eyes, spec+code only).`)

const perUnit = await pipeline(
  UNITS,
  // Stage 1: the section auditor.
  (u) => agent(u.prompt, { label: u.label, phase: 'Audit', schema: FINDER_SCHEMA }),
  // Stage 2: adversarial verification, one skeptic per candidate drift.
  (finding, u) => {
    if (!finding || !finding.drifts || finding.drifts.length === 0) {
      return Promise.resolve({ unit: u.key, derived_properties: finding ? finding.derived_properties : [], faithful_matches: finding ? finding.faithful_matches : [], verified: [], finder_summary: finding ? finding.summary : 'no result' })
    }
    return parallel(finding.drifts.map((d, i) => () =>
      agent(`${DISCIPLINE}

ADVERSARIAL VERIFICATION. A section auditor reported this candidate DRIFT between spec
rev2 and the verified code. Your job is to INDEPENDENTLY re-derive and either CONFIRM,
REFUTE, or RECLASSIFY it. Default to skepticism: open the actual code and the actual spec
text yourself; do NOT trust the auditor's quote — verify it. A drift survives only if the
spec genuinely promises something the 'ensures' does not deliver (or a 'requires' genuinely
excludes a spec-admitted case that is NOT handled elsewhere).

CANDIDATE DRIFT (unit ${u.key}):
  title: ${d.title}
  classification claimed: ${d.classification}
  spec_anchor: ${d.spec_anchor}
  spec_says: ${d.spec_says}
  code_anchor: ${d.code_anchor}
  code_proves (auditor's reading): ${d.code_proves}
  evidence: ${d.evidence}
  severity: ${d.severity} | proposed_disposition: ${d.proposed_disposition}

Do this:
1. Re-read the cited spec section at ${SPEC}. Quote the actual governing sentence.
2. Open the cited code (file:line). Read the ACTUAL 'requires'/'ensures'/'spec fn'. Quote
   the actual clause — confirm or correct the auditor's reading.
3. If D2 (precondition hides a case): you MUST locate where the excluded case is handled
   (give file:line) OR establish it is genuinely impossible OR confirm it is unhandled.
   Put the result in 'excluded_case_resolution'.
4. Verdict: confirmed (real drift, class stands), reclassified (real drift, different D-
   class — give it), or refuted (not a drift: the ensures DOES deliver the spec property,
   or the spec never promised it, or the excluded case is handled). Set final_classification
   to 'not-a-drift' if refuted.
5. Set a fair final_disposition: fix-now (small, faithfulness-restoring change), follow-on
   (tracked, out of closeout scope), accepted-documented (spec or a code comment gains an
   explicit honest note), or none (refuted). Remember the deliverable's principle: NO drift
   is closed silently — even an accepted deviation must be documented somewhere.`,
        { label: `verify:${u.key}#${i + 1}`, phase: 'Verify', schema: VERIFY_SCHEMA })
        .then((v) => ({ unit: u.key, drift: d, verdict: v }))
        .catch(() => null)
    )).then((verified) => ({
      unit: u.key,
      derived_properties: finding.derived_properties,
      faithful_matches: finding.faithful_matches,
      finder_summary: finding.summary,
      verified: verified.filter(Boolean),
    }))
  },
)

const units = perUnit.filter(Boolean)
const allVerified = units.flatMap((x) => x.verified || [])
const surviving = allVerified.filter((x) => x.verdict && x.verdict.verdict !== 'refuted')
const refuted = allVerified.filter((x) => x.verdict && x.verdict.verdict === 'refuted')
log(`Audited ${units.length} units. Candidate drifts: ${allVerified.length}; survived verification: ${surviving.length}; refuted: ${refuted.length}.`)

phase('Synthesize')
const ledger = await agent(`${DISCIPLINE}

You are writing the final DRIFT LEDGER deliverable: doc/results/69_verus-findings.md, the
fresh-eyes audit confirming whether the Verus-verified code implements spec rev2.

You are given the SURVIVING drifts (confirmed or reclassified by an adversarial verifier),
the REFUTED candidates (record briefly that they were checked and dismissed), the auditors'
spec-derived properties, and the faithful-match confirmations. Produce a complete, honest
Markdown ledger.

Required structure:
  # 69 — Verus drift audit against spec rev2 (fresh-eyes re-derivation)
  - A short intro stating the method (judged ONLY against spec + code; justification prose
    deliberately ignored) and the headline verdict (how faithful is the verified code).
  - "## Watch-list resolution" — explicitly resolve the three pre-flagged items: (1) revoke
    root-survival / !is_homed vs "revoke destroys all descendants" + the seL4-zombie case;
    (2) phase-8 commit-recovery = structural/arithmetic half, content-coverage to TLA+, and
    whether anything reads as "fully mechanized" when it is not; (3) refcount_sound claimed
    as a system invariant vs proven per-op-conditionally. Each with a clear disposition.
  - "## Drift ledger" — a table AND per-drift detail. For each surviving drift: ID (e.g.
    D-A1), title, classification (D1/D2/D3/D4), spec anchor, code anchor (file:line + clause),
    spec-says vs code-proves, severity, and DISPOSITION (fix-now | follow-on |
    accepted-documented) with the exact text/edit the disposition implies (e.g. the honest
    note the spec or a code comment should gain). NO drift closed silently.
  - "## Refuted candidates" — one line each: what was claimed, why it was dismissed.
  - "## Faithful matches" — the properties where code genuinely matches spec (the audit's
    positive findings), grouped by section.
  - "## Inputs to 9e" — the concrete spec/CLAUDE.md edits the accepted-documented dispositions
    feed (generalizing the §4.8 phase-8 discipline of stating proof boundaries honestly).

Be precise and fair: a disposition of 'accepted-documented' or 'follow-on' is correct when
the code is sound but the proof boundary or a precondition needs an honest note; reserve
'fix-now' for small faithfulness-restoring changes. Group related drifts (e.g. the
refcount_sound per-op clauses) rather than listing 8 near-duplicates. Return ONLY the
Markdown body (it will be written to the file).

=== SURVIVING DRIFTS (confirmed/reclassified) ===
${JSON.stringify(surviving, null, 1)}

=== REFUTED CANDIDATES ===
${JSON.stringify(refuted.map((r) => ({ unit: r.unit, title: r.drift.title, claimed: r.drift.classification, why: r.verdict.reasoning })), null, 1)}

=== SPEC-DERIVED PROPERTIES (per unit) ===
${JSON.stringify(units.map((u) => ({ unit: u.unit, derived: u.derived_properties, summary: u.finder_summary })), null, 1)}

=== FAITHFUL MATCHES ===
${JSON.stringify(units.map((u) => ({ unit: u.unit, matches: u.faithful_matches })), null, 1)}
`, { label: 'synthesize-ledger', phase: 'Synthesize' })

return {
  counts: { units: units.length, candidates: allVerified.length, surviving: surviving.length, refuted: refuted.length },
  surviving,
  refuted: refuted.map((r) => ({ unit: r.unit, title: r.drift.title, why: r.verdict.reasoning })),
  ledger_markdown: ledger,
}

After all the subagents were done, this was the response:

>The audit is complete. doc/results/69_verus-findings.md is written (833 lines, 22-row drift ledger with per-drift detail, dispositions, refuted candidates, faithful-match positives, and the 9e inputs).

> ## How it was done

> A fresh-eyes ultracode workflow: 8 section-auditors (each derived the spec-mandated property before opening any ensures, then read the verified code) → adversarial verifier per candidate (re-opened spec+code, default-skeptical) → synthesis. 35 candidates → 24 survived, 11 refuted. I then independently re-verified by hand the two high-severity findings and all three watch-list items against the actual requires/ensures and the kernel call path — every one held. > ## The verdict > The verified code is substantially faithful — where Verus proves something, it proves it well (∀-quantified rights monotonicity, transitively-complete descendant deletion, faithful FIFO/waiter Seq models, total mount/replay bounds, absorbing at-most-one terminal report). The real gaps: > - D-A1 (high): revoke's !is_homed precondition is false for every real CapRevoke syscall — cur_slot always resolves a cspace cell (homed), the wrapper is unverified, and there's no verified caller in kcore. So the proven contract (descendant-deletion included) is vacuous over actual inputs; on the real path it's witnessed only by a unit test. The fix is a contract split, and it's the top-priority follow-on.

• D-B1 (high): §5.4's "priority ceiling is a value on the cap, attenuates monotone" is unmodeled — CapKind::Thread has no priority field; enforcement is an unverified shell if prio > current().priority.
• Watch-list resolutions: (1) descendant-destruction is unconditional, only the non-spec root-survival is gated by !is_homed, and the spec admits the seL4-zombie self-empty; (2) commit-recovery is the structural/arithmetic half — content_ok_spec is uninterp, content-coverage is a genuine TLA+ seam, and that's spec-consistent (§6 routes it to TLA+); (3) refcount_sound is a faithful model preserved per-op but not an established/threaded system invariant — the "system invariant" comment language overstates it, though the spec's retype-exclusivity linchpin rides the watermark+CDT, not refcount.

> The most consequential reconciliation I made over the raw workflow output: the unit-E "leaf ops carry no refcount obligation" finding (kept) vs the unit-H "chain not closed / not a system invariant" framing (refuted) — I confirmed in code that signal exports the bridge, wait/disarm export exact deltas but not the bridge, and arm exports neither — so the genuine residue is the leaf-op export gap (D-E1/D-F2), not a spec violation. Every accepted/fix-now item is routed into the §6 + boundary-note edits for 9e. > One scope note: the kernel/ shell files D-A1/D-B1 cite are present and say what's claimed, but they're the unverified architectural shell — the findings about them are statements about what the verified ensures don't reach, not about runtime correctness (the code runs the same; preconditions erase). I did not apply the D-F2 fix-now code change — per the task, that's a recommendation feeding 9e, not part of the audit deliverable.

The first finding was an implication of the form if false then useful-property, oops. The second was verification skipped altogether. The full list is in 69verus-findings.md.