The important, durable development notes for this project live in claude-notes/ — read claude-notes/README.md before working on the Rocq/Iris proofs under iris/. Start with claude-notes/durable-notes.md (guiding principle, build instructions, cross-cutting gotchas), then open the claude-notes/design/ file for the subsystem you are touching and, only if you are working on that effort, the relevant claude-notes/projects/ worklist. The notes are split by topic so you can read just the relevant parts without wading through unrelated in-flight worklists.