By 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):
State the method's specification: preconditions, postconditions, concurrent behavior promises.
Identify the synchronization protocol ensuring the postcondition.
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
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.