Audit Correctness Proof

Attempt formal correctness proofs for all public cache methods

ben-manes Updated

File contents

Attempt to PROVE the correctness of the cache, not to find bugs.

For each public method (get, put, remove, compute, computeIfAbsent, merge, replace, size, clear):

  1. State the method's specification: preconditions, postconditions, concurrent behavior promises.

  2. Identify the synchronization protocol ensuring the postcondition.

  3. Write a proof sketch: a. Assume the precondition holds b. Identify the critical section(s) c. Show the postcondition is established within the critical section d. Show no concurrent operation can invalidate it before the caller observes

  4. If you CANNOT complete the proof at any step, stop and report:

    • Which step fails
    • What additional assumption would be needed
    • Whether the code guarantees that assumption

Gaps in the proof are more valuable than speculative bug reports — a gap tells us exactly where to look.

Do not provide praise or style commentary.

ben-manes/caffeine/tree/main/.claude/skills/audit-correctness-proof commit 151904a148

Frequently asked questions

npx skillmds@latest add ben-manes/audit-correctness-proof