Eunomia OS - audits, profiling, improvements

This is the fourth in a series of blog posts about my experimental operating system, Eunomia.

Full repo audit

Encouraged by the results of the previous audit-and-fix work, I decided to do it on the whole repo. This time, I put a little more effort into the prompt, and actually wrote it myself:

>Hello! Please review how the project conform to the spec doc/spec/specrev0.md Break the analysis down into:

># What to look for
>## Cosmetic issues - fix these as you go >1. Stale references to spec's section (note: the project introduced a rule to always use the revision number together with section number to keep track of documentation drift, like "rev0§6.2" to refer to revision 0, section 6, subsection 2. None of the comments or other documentation follows that rule other than CLAUDE.md itself, so this will need to be amended).
>2. Historical baggage in comments - comments should explain why the code is structured like it is now. Interesting past developments may be recorded in the appropriate section of the spec, but not in comments. The only exception is that if some implementation is not obvious and motivated by past errors, but still do your best to word it in a way to describe why is it like this now, not why it isn't something else.

>The current version of the spec was blessed as revision 0. References to any other revisions should be treated as stale.
>When removing anything from the comments, do not mention that anything was removed, just leave the comments in a state suitable for the future. If anything should be recorded for posterity, write it down in the output document. >## Incorrect implementation or verification >Look for any code that doesn't do what the spec says. >Note it in the result only, without attempting ad-hoc corrections. >Do not be swayed by the volume of proofs and other verification in this project. There are many ways to write a lot of verification without actually verifying anything of substance, like:
>a) Verus proofs with important work skipped by assume, external_body, etc. (these should be only used for parts that are genuinely unverifiable with Verus, or belong to external projects. Nothing in this project is a priori out of scope for verification, if Verus can be used for a task, it should) >b) Verus or TLA+ specs with always false premises, thus proving vacuously true implication >c) Tests that cannot be failed by any code due to their construction >d) Tests or proofs that don't involve any real code paths. Note however that if the tests/proofs check something that the spec says, but the code doesn't do, then treat it as an implementation deficiency, and leave the verification as future proofing >e) Mocks and placeholders that break the entire point of code that is using them >f) Using tools in a way that defuses them (modeling large fragments as atomic steps in TLA+ when they aren't atomic in the real processes. Using Shuttle for code that needs non-SeqCst orderings, as it will model them as SeqCst anyway. Another example is using Loom for Relaxed orderings, which it doesn't faithfully model - but not using Loom for SeqCst, which it models as AcqRel - in that case Loom may still be a better tool than Shuttle due to its soundness if the performance allows, but possibility of false positives should be taken into account) >h) Likely there are many more ways to write verification theater that doesn't do anything, please report anything suspicious

>## Incomplete implementation
>If it's in the spec, but not in the code, report it >## Incomplete verification >All code in the project should be subject to some sort of verification. The only part of the project's source that's truly out of scope for verification are the platform specific assembly parts. Code outside the project (the Rust compiler, external libraries, correctness of the verification tools itself) is also out of scope. >Write down any parts of the project that are unverified, or use a suboptimal tool for verification. >## The spec itself may be deficient >Is there anything that the project does better than the spec? Are any parts of the spec ambiguous, while the project resolves it? Write this down too. ># Review procedure >Since this is a large task, use ultracode workflows to structure it and break it down into manageable pieces. Write your findings in doc/results/auditrev0.md

The comment issue was a constant bane of this project. Claude defaulted to writing elaborate comments with histories of everything done to the code ever. Verification theater review was a continuation of the previous work. Then the gaps in the spec and the code.

After thinking rather hard and spawning 68 subagents, Opus produced auditrev0.md. The "rev0" is because I rolled back the spec revision numbers from rev3.

All in all, not too bad. I took 4 days to fix all of this, with two followups.

Verus profiling

I started by adding a copy of Verus' standard library to the references, and some tutorials to docs. Then I asked Claude to establish a proper baseline for profiling:

Hello! This project recently gained a script to establish a profiling baseline for Verus proofs: scripts/verus-baseline.sh (it wasn't yet used for any real profiling, so feel free to modify it if it's inadequate). Please do the following:

Establish the timing data for the entire crate as it is now

Read file doc/guidelines/verus-computation.html doc/guidelines/verus-local-proofs.html doc/guidelines/verus-modules.html doc/guidelines/verus-quantifier-profiling.html doc/guidelines/verus-smaller.html doc/guidelines/verus-structured-proofs.html for ideas on optimizing Verus proofs

Scan the repo for all Verus proofs that could be optimized using these techniques, or simplified some way (such as by regular refactoring, or using the Verus standard library - code checked out in reference/vstd - better that it is now)

>Then please write a plan in doc/plans/0verus-optimization.md with candidates for optimization (include everything that looks promising now, sorted from the most likely to be impactful to the least), and instructions to try out each in succession, and at each step monitoring: >a. Does the crate still verify (if not, the work needs to be reverted) >b. Check if the verification got faster, and if the code is cleaner (compare against baseline and the previous result) >c. Optimization tasks must make the code faster, and should not make the code too much harder to understand >d. Conversely, simplification tasks must make the code easier to understand, but should not make the code too much slower >As much as feasible (but don't drop potentially good ideas if they don't fit this), the plan should split the tasks into separately implementable attempts, so the later implementation can pick and choose the ones that worked and are worth it. >Since this is a large effort, use ultracode workflows to structure it (in particular the repo scanning task in (3) may need them). After you're done, commit your work, and open a PR

The result: 0verus-optimization.md. This took a day, and did manage to make the Verus code a bit faster. Another thing I got out of it were updated guidelines.

TLA+ optimization

The properties checked by TLA+ specifications are divided into safety properties ("nothing bad can happen") and liveness properties ("good will happen"). Of these, safety properties are easier to manage in general, as they only require checking that some given forbidden states are unreachable. Meanwhile, liveness properties require tracking the history of state transitions.

First, I meant to focus on safety. I started by dropping downloaded websites (specifically, Optimizing model checking and Model values and symmetry) and advice I've got from chatgpt into the docs folder. Then, as usual, I asked Claude for a plan. Since it found some opportunities for improving the liveness checks too, I didn't argue.

That run was largely uneventful. Safety properties are, well, safer to optimize. You can use SYMMETRY and such. The effort made the TLA code a bit faster, but only by parallelizing the liveness arm. Worth a try, I guess.

For further liveness work, I dropped some docs again ("Liveness" section of the PlusCal tutorial, as well as TLC Model Checker, and Using Coverage pages of the TLA+ wiki), again with chatgpt advice. Then, a plan.

>I've read the plan. Tier 2 — Step 4 is a fairness reformulation probe: test whether replacing the per-cap fairness Fairness == \A c \in CapIds : WF_crVars(RevokeStep(c)) with a single existential WF_crVars(\E c \in CapIds : RevokeStep(c)) still proves EventuallyRevoked. The expected outcome is a livelock → revert the weakening, but harvest a new negative control CapRevocation_NegFairness.cfg, wire it into the runner + manifest, and write findings doc 15_tla-findings.md.

>All agents have reported and I have the full picture. Before finalizing, I need to sharpen a key prediction: whether the single-existential WF actually livelocks at the 4-cap floor (the plan's expectation) or whether EventuallyRevoked might still hold there (the plan's hedge: "If it holds → a stronger theorem"). That hinges on whether the floor has enough caps to sustain a "churn-one-subtree-while-starving-another" lasso. Let me read Init, RevokeBegin, Copy, and the Copy guard to refine this.

>I now have a complete picture. One analysis result materially shapes the deliverable, so let me work through it before finalizing.

Key analysis — will the single-existential WF actually livelock at the 4-cap floor? The plan expects a livelock, but I worked through the reachability and I don't think it livelocks at the floor:

>- Init seeds exactly one live cap (InitCap); everything else derives from it via Copy. The Copy guard ~AncestorOrSelfRevoking(src) forbids growth into any revoking subtree, so a fixed revoking subtree only ever shrinks.

>- Under WF_crVars(\E c : RevokeStep(c)), if the victim cap is the only revoking cap with a leaf, the existential is continuously enabled and WF forces it to fire — draining the victim. To starve a victim, you need a second, independently-refilled revoking subtree to keep the existential "busy" on another cap. >- Two disjoint (non-nested) revoking subtrees both hanging off a non-revoking common root require, at peak, 5 simultaneously-live caps (root + victim-root + victim-leaf + churn-root + churn-leaf). The floor has only 4.

>So my prediction: EventuallyRevoked holds at the 4-cap floor under existential WF — the starvation lasso needs CapIds=5. The probe (running TLC) will confirm or refute this. This matters because it changes the artifact: a floor control wouldn't livelock, so the negative control likely needs CapIds=5. As a negative control, TLC stops at the first lasso (it doesn't exhaust the space), so it can stay cheap — but that intersects your recorded concern that CapIds=5 blows the CI budget for the exhaustive arm.
>This one fork is genuinely your call, so let me confirm how to handle it.

I chose to try CapIds=5.

>SANY passes. Now run the floor probe (CapIds=4). If it holds (predicted), it's a full exploration (~2 min at 4 workers); if it livelocks, it stops early. I'll run it in the background and poll the log.

Then it ran this (after all, why run many command when one command do trick):

mkdir -p scratch-step4 && rm -rf target/tla-states/probe-NegFairness-c4 && \\ TLC_WORKERS=4 TLC_METADIR=\"target/tla-states/probe-NegFairness-c4\" TLA_JAVA_OPTS=\"-Xmx4g\" \\ bash tools/tla/tla-model-check.sh tla/cap_revocation/CapRevocation.tla CapRevocation_NegFairness.cfg \\ </dev/null >scratch-step4/probe-c4.log 2>&1\necho \"EXIT=$?\""

Some time later:

>The early temporal check at 164,424 states found no violation — the floor run is doing a full state exploration, consistent with my prediction that EventuallyRevoked holds at CapIds=4 (the reachable set under SpecExistFair equals Spec's, since fairness doesn't change reachable states). It will run to completion (~2 min) and report "No error found." Let me wait for it to finish before escalating to CapIds=5 (serial, to keep timing clean).

Meanwhile, TLC finished:

1 === TLC done === 2 Semantic processing of module TLC 3 Semantic processing of module CapRevocation 4 Linting of module CapRevocation 5 Starting... (2026-06-25 15:05:50) 6 Implied-temporal checking--satisfiability problem has 4 branches. 7 Computing initial states... 8 Finished computing initial states: 1 distinct state generated at 2026-06-25 15:05:50. 9 Checking 4 branches of temporal properties for the current state space with 164424 total distinct states at (2026-06-25 15:05:53) 10 Finished checking temporal properties in 00s at 2026-06-25 15:05:53 11 Progress(9) at 2026-06-25 15:05:53: 178,157 states generated (178,157 s/min), 41,106 distinct states found (41,106 ds/min), 23,288 states left on queue. 12 Checking 4 branches of temporal properties for the current state space with 1713828 total distinct states at (2026-06-25 15:06:53) 13 Finished checking temporal properties in 08s at 2026-06-25 15:07:02 14 Progress(16) at 2026-06-25 15:07:02: 3,633,414 states generated (3,455,257 s/min), 428,457 distinct states found (387,351 ds/min), 49,448 states left on queue. 15 Progress(22) at 2026-06-25 15:07:26: 4,831,322 states generated, 503,070 distinct states found, 0 states left on queue. 16 Checking 4 branches of temporal properties for the complete state space with 2012280 total distinct states at (2026-06-25 15:07:26) 17 Finished checking temporal properties in 12s at 2026-06-25 15:07:39 18 Model checking completed. No error has been found. 19 Estimates of the probability that TLC did not check all reachable states 20 because two distinct states had the same fingerprint: 21 calculated (optimistic): val = 1.2E-7 22 based on the actual fingerprints: val = 6.9E-9 23 4831322 states generated, 503070 distinct states found, 0 states left on queue. 24 The depth of the complete state graph search is 22. 25 The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 29 and the 95th percentile is 3). 26 Finished in 01min 49s at (2026-06-25 15:07:39) 27

>Floor probe confirmed (Branch B): EventuallyRevoked HOLDS at CapIds=4 under single-existential WF — "No error has been found," exit 0, 503,070 distinct / diameter 22 / 4,831,322 generated (byte-identical to the real arm), 1m49s at workers=4. My prediction holds: the floor is below the 5-cap threshold for the starvation lasso.

>Now I escalate the control to CapIds=5 and confirm it livelocks under the exact neg-control invocation (TLC_WORKERS=1 -Xmx2g, periodic liveness checking), measuring cost for the budget check.

Then it wrote a negative control for 5 capabilities, and it indeed failed:

1 ok CapRevocation_NegControl.cfg LiveParent violated as expected (exit 12) 2 ok CapRevocation_Safety_NegControl.cfg LiveParent violated as expected (exit 12) 3 ok CapRevocation_AsymBug.cfg DeadNowhere violated as expected (exit 12) 4 ok CapRevocation_CapAsymBug.cfg DeadNowhere violated as expected (exit 12) 5 ok CapRevocation_ThreadAsymBug.cfg FireSafe violated as expected (exit 12) 6 ok CapRevocation_ReportMonotoneBad.cfg ReportMonotone violated as expected (exit 13) 7 ok CapRevocation_NegLiveness.cfg EventuallyRevoked violated as expected (exit 13) 8 ok CommitProtocol_NegControl.cfg RecoverReconstructs violated as expected (exit 13) 9 ok CommitProtocol_AsymBug.cfg RecoverReconstructs violated as expected (exit 13) 10 ok IpcReactor_NegControl.cfg NoLostWakeup violated as expected (exit 12) 11 ok IpcReactor_NegBackpressure.cfg NoLostWakeupWritable violated as expected (exit 12) 12 ok IpcReactor_NegLostWakeup.cfg NoLostWakeup violated as expected (exit 12) 13 all 12 negative controls failed as designed 14

Pretty neat that Opus figured it out on its own by just predicting the next tokens.

This time, the liveness arm was truly optimized a bit but I decided to spend the budget on more coverage.

Finally, guidelines.

Concurrency verification with Verus

Since feeding docs to Claude worked so well, this time I dropped Travis Hance's thesis after converting it to text, together with scraped Verus docs. Then, a plan.

Also,

Anti-theatre teeth

Calm down there, buddy.

I forgot to tell Opus where to write the review:

>Hello! Since commit 8bd5bb4df58ac1fda386836979980b482809966f this project underwent an effort to use Verus more extensively, in particular (but not limited to) the concurrent parts. Please review (independently, without taking the written justifications at face value) if: >1. Is the new code sound? Are any replacements of existing tool usage done correctly? Are any omissions justified? >2. What are the reasonable follow ups? Should the deferrals be reconsidered? >3. Was the comment and justification discipline upheld? >Since this is a large task that will involve reading a lot of files and documentation, use ultracode workflows to structure it.

So it dutifully wrote it inline:

>All spot-checks confirm the agents' findings. I now have everything needed to synthesize. Here is the consolidated review.

>---
># Review: the Verus-extension effort (commits 8bd5bb4..f72b2ef, Tasks 1–13) >Bottom line: the effort is sound. I re-ran the prover from cold myself (not trusting the docs), fanned out 13 independent per-task soundness reviewers each followed by an adversarial refutation pass, and ran four cross-cutting audits. Every adversarial refutation failed to break its claim, every gated crate re-verifies with the exact counts claimed, and the trusted-seam tally is provably unchanged. The only defects are one comment-discipline slip and a small set of low-severity scope/robustness notes. >## Ground truth I established independently >A cold per-crate cargo clean -p X && cargo verus verify under the correct pin (0.2026.06.07.cd03505, toolchain 1.95.0; submodule at release/rolling/0.2026.06.07.cd03505) reproduced every claimed count, all exit 0, all with a real verification results:: line (not stale cache): >kcore 406 · cas 77 · ipc 71 · freelist 29 · dma-pool 0 · virtio-blk 3 · storage-server 19 · loader 18 — all ✅. >Re-derived trusted-seam tally = 14, and the seam-bearing lines are byte-identical base→HEAD: no new external_body/assume_specification, zero bare in-proof assume(, no fabricated axioms. So "tally stays 14, no new seam" is true, not asserted. >## 1. Is the new code sound? Are replacements correct? Are omissions justified? >Sound — yes, across all 13 tasks. The substantive points: >- The proofs have teeth, not vacuity. The two highest vacuity-risk tasks survive scrutiny. Task 9's FIFO labels (channel.rs) name real Seq::push/drop_first/Err-frame content — not the length ring_fifo().len()±1 the guideline warns is vacuous — and they key the correct ring index (end_idx_spec(end) for send vs 1 - end_idx_spec(end) for recv), avoiding the bidirectional-conflation hazard the plan itself flagged. Task 13's recover_reconstructs is a projection of its own producer's ensures, but its committed teeth lemma lemma_recover_reconstructs_pins_head (cas/src/store.rs:1657) genuinely fails for a wrong head — I confirmed the off-by-one (wal_head+1) experiment is reverted and the pins lemma is the load-bearing residue.
>- Register-path coherence (Task 6) is the real win. The coherent slot/used bijection invariant is genuinely load-bearing: the adversarial pass showed the postcondition is unprovable without the requires coherent precondition, so it is not decorative. >- Replacements done correctly. No TLA safety arm was retired or duplicated — every routing note keeps the global/liveness arms TLA-owned and only mechanizes the local per-step half. All "kept" oracle tiers actually survive: the three reactor proptests, the Loom + Shuttle seqlock harnesses, the fuzz corpora, and the TLA negative controls are all present and unmodified (verified by diff, not by trust). >- Omissions justified. The biggest scope honesty test — Task 8's "postcard body stays trusted by feature-exclusion, not external_body" — is sound: dropping serde under --no-default-features removes the body codec from verified compilation entirely, so there is genuinely nothing to mark, and check_header (the part that does ship in every build) is proven total and composes on the already-verified ipc::version_ok.

>Low-severity soundness/scope notes (none block correctness):

>- virtio-blk/src/lib.rs:240 — new() does (max as u16).min(8) with no .max(1); a device reporting QUEUE_NUM_MAX as a nonzero multiple of 65536 truncates queue_size to 0, which would divide-by-zero in avail_ring_slot. This is on the trusted MMIO bring-up path outside verus!{} (the proof correctly requires qsize ∈ 1..=8), so it's a latent robustness gap in the trusted seam, not a proof hole. Cheap fix: .min(8).max(1). >- Task 4 (storage-server) — the verified attenuate/has_right/lemmas characterize the rights algebra, but the running authorization guards (lib.rs:546, :896) are plain Rust and don't reference the verified spec. Meaningful proof, but the exec dispatch isn't tied to it (the usual verified-core/plain-shell seam). >- Task 6 — the slots.len()==64 conjunct of wf is type-implied (cosmetic); the new "bind-failure leaves reactor untouched" fix is structurally correct but untested (the model transport's bind is infallible).

>## 2. Reasonable follow-ups / should deferrals be reconsidered?
>The §4 deferrals are correctly closed — I verified the load-bearing technical claims against the pinned prover source:
>- urt seqlock family stays deferred correctly: vstd/atomic.rs is hardcoded SeqCst with no fence anywhere, so a Verus proof would certify a different binary than the Relaxed+fence ship code. This is a genuine prover-capability gap, not retired by the onboarding risk being gone. Keep Loom as proof-of-record. >- heap-arena PointsToRaw stays deferred: still no path to mint a PointsToRaw for a static [u8;N] under the pin, and the disjointness it would prove is already discharged by the freelist dep. >- the *-NONO state-machine rewrites stay deferred: the reactor is genuinely single-threaded (&mut self, no atomics), so tokenized SMs bind to nothing.

>Genuine follow-ups, in priority order:

>1. caprevoke-movesemantics-single-owner per-op subset (medium). The full global single-owner invariant is rightly deferred (XL global rewrite), but the per-op "move-conservation" ensures on send/recv/bind with a DupOwner teeth control is now lower-risk than when scheduled — this effort proved out exactly the projection+teeth-on-cap-slot-views technique it needs. This is the strongest next Verus task. >2. Fix virtio-blk queue_size clamp (the qsize=0 note above) — small, real. >3. Stale plan justification (medium, doc-only): §4's reason for deferring ipc-reactor-protocol-tsm cites "the macro crate is off-crates.io" — factually wrong now: verus_state_machines_macros resolves from crates.io (Cargo.lock:1011), as findings doc 0 already established. The conclusion (don't pursue) still holds on its other reasons, but the plan prose should be reconciled.

>## 3. Was comment/justification discipline upheld?
>Almost entirely, with one fix needed:
>- One medium violation: cas/src/store.rs:1650 — /// **Anti-theatre teeth** (Task 13): …. This is the only (Task N) reference in any .rs file in the tree (I grepped). It cites the plan's task numbering (a forbidden doc/plans reference) and is "what-was" framing. Trivial fix: strike "(Task 13)". >- One low/pre-existing note: several new comments cite tla/.../*.tla:NNN paths (store.rs:1241/1251, channel.rs, cspace.rs). Strictly, CLAUDE.md allows only doc/spec/doc/guidelines paths — but this extends an established convention (ipc/src/reactor.rs already cited tla/... at the base commit), so it's a consistency-vs-letter tension, not a regression introduced here. >- Otherwise clean: every spec reference carries its rev2§ revision, no what-was/removal-history narration, no comment-to-comment references, no doc/results citations in code. The vendor swap is clean — reference/vstd/ is referenced only in findings doc 0 (which is exempt and documents the deletion); no crate, build file, or comment points at it.

>The findings-doc procedure was followed well: every doc records numeric counts/rlimit (the doc-only tasks correctly state why there's no delta rather than faking one), and every claimed revert is actually gone from the tree (the state_machine! pilot, the (wal_head+1) experiment, the destroy_tcb measurement experiment — all confirmed absent).
>--- >### Concrete action items
>1. cas/src/store.rs:1650 — remove "(Task 13)" from the comment (medium, discipline). >2. virtio-blk/src/lib.rs:240 — clamp queue_size to ≥1 to close the trusted-path div-by-zero (low, robustness). >3. Plan doc/plans/0_verus-concurrency.md §4 — drop the stale "off-crates.io" reason from the ipc-reactor-protocol-tsm deferral (low, doc accuracy). >4. Optional next task — the per-op move-conservation ensures for cap move-semantics; the technique risk is now retired.

>Nothing here is load-bearing against soundness — the verification is real, reproducible, and honestly scoped. Items 1–3 are minor cleanups.
>Want me to apply the three cleanups (1–3)? They're small and low-risk.

I did want Opus to apply the cleanup, so and it did.

Then more guidelines, with some general ones, and a new spec revision too.

Further Verus improvements

With all the new guidelines, it was time to apply them repo-wide. As always, first a plan.

>Give lemma_two_allocs_disjoint mechanical teeth

You know, I'm not even going to argue.

Since this work was relatively minor, I didn't bother with a review this time.