audit-correctness-proof

name	audit-correctness-proof
description	Attempt formal correctness proofs for all public cache methods
context	fork
agent	auditor
disable-model-invocation	true

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.