This is the third in a series of blog posts about my experimental operating system, Eunomia.
Kani
First, a scratchpad crate to check if it's really working this time. Then, I asked Fable to write a plan for the rewrite. It helped that I already had a pile of TLA+. Of the features planned, the CI job was probably the worst idea, I wasted inordinate amount of my time and Github's compute for that.
Fable only managed to write the saved plan itself, and a temporary plan mode plan for the first task (capability spaces). I ran into a session limit, and woke up to an announcement.
Fortunately, Opus was more than enough. It even kept signing commits as Fable anyway, perhaps to help with morale.
The Kani rewrite found some bugs. In general, the idea of asking Claude for a results file for each task was useful in the future. I closed with asking Claude for a review.
The review got me worried a bit, not the content itself but the phrasing:
The plan was implemented faithfully, with good engineering judgment and an unusually honest record of its own limits.
This sort of self-glazing was a recurring pattern, and got me thinking that I'm likely not asking for reviews that are adversarial enough. My prompt was:
>Hello! Please read doc/plans/0kani-rewrite.md which should be already implemented (the latest doc changes and cleanups are sill in Github CI, but tests passed locally, so you can assume that lands eventually) and review how the state of this repo conforms to it. See also the intermediate reports in doc/results. Was the plan implemented correctly? Are any modifications justified? Do you have any other remarks and comments? When in doubt, refer to the spec in doc/spec/2specrev2.md and the TLA+ code in the tla directory. Write your final report in results/9kani-review.md
Loom and shuttle
Again, first a scratchpad , then a plan. Later, guidelines
My next review prompt wasn't particularly more adversarial:
>Hello! Please read doc/plans/2ipc.md and review and criticise the current (PR #44 is still in CI, but it's on Kani verification now, which shouldn't be relevant for IPC, so treat it as merged for the purpose of the review) implementation. What was done? What wasn't? Was the plan done correctly? Are any alterations justified? What remains to be done? Write your review in doc/results with the same naming scheme as existing documents.
The review was somewhat less self-aggrandizing still.
The next task was rewriting large parts of the code in Verus, finally.