@@ -846,6 +846,9 @@ jobs:
           fi
           echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'lr'.*'LeakyReader'" \
             || { echo "FAIL: a non-empty-Dispose local (LeakyReader) must still leak (#225 stays scoped)"; exit 1; }
+          # Codex P2: an empty SYNC Dispose but a real DisposeAsync (a `*Reader` here) must still leak.
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'ar'.*'AsyncReader'" \
+            || { echo "FAIL: a type with a real DisposeAsync (empty sync Dispose) must still leak (#225)"; exit 1; }
           echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) + OWN014 (static-event region escape) + DI001 (captive dependency) + DI002 (scoped captured weakly) + DI003 (transient IDisposable captured by a singleton) + DI004 (transient IDisposable service-located from the root provider) + DI005 (scoped service cached from a created scope) + [OwnIgnore] suppression (silent-but-counted, SARIF suppressions) + #218 DP old->new subscription rotation (silent; controls flagged) + #225 empty-Dispose local exemption (silent; controls flagged) at the C# location"
       - name: Flow-sensitive local IDisposables (--flow-locals, P-016 B0b/B2)
         run: |
@@ -1088,11 +1091,15 @@ jobs:
             || { echo "FAIL: #225 flow: a non-empty *Reader local must still leak"; exit 1; }
           echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'d' is never disposed" \
             || { echo "FAIL: #225 flow: an empty override over a real base Dispose must still leak"; exit 1; }
-          # exactly 3 EmptyDisposeSample findings -> the two empty-Dispose locals (the enumerator and
-          # ScratchReader) are SILENT; any leak would push the count past 3.
+          # Codex P2: an empty SYNC Dispose() but a real DisposeAsync() (IDisposable + IAsyncDisposable)
+          # must NOT be exempted — the real cleanup is async and the flow detector treats it as a release.
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'ar' is never disposed" \
+            || { echo "FAIL: #225 flow: a type with a real DisposeAsync (empty sync Dispose) must still leak"; exit 1; }
+          # exactly 4 EmptyDisposeSample findings -> the two provably-empty-Dispose locals (the enumerator
+          # and ScratchReader) are SILENT; any leak of them would push the count past 4.
           n225=$(echo "$out" | grep -cE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN00")
-          [ "$n225" = "3" ] \
-            || { echo "FAIL: #225 flow: expected exactly 3 EmptyDisposeSample findings (controls only), got $n225"; exit 1; }
+          [ "$n225" = "4" ] \
+            || { echo "FAIL: #225 flow: expected exactly 4 EmptyDisposeSample findings (controls only), got $n225"; exit 1; }
           echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, #225 empty-Dispose local exempt, beyond flat)"
       - name: Gallery C#-native bad/ok pairs (examples/gallery/cs/)
         run: |
 
@@ -1324,6 +1324,12 @@ static bool HasEmptyDisposeBody(ITypeSymbol? t)
     for (var b = nt.BaseType; b is not null && b.SpecialType != SpecialType.System_Object; b = b.BaseType)
         if (ImplementsIDisposable(b))
             return false;
+    // A non-empty DisposeAsync() can do the REAL cleanup even when the sync Dispose() is an empty
+    // compatibility no-op (a type implementing both IDisposable AND IAsyncDisposable). The flow
+    // detector already treats DisposeAsync() as a release, so an undisposed local of such a type is a
+    // real leak — conservatively refuse to exempt any type that declares its own DisposeAsync (Codex).
+    if (nt.GetMembers("DisposeAsync").OfType<IMethodSymbol>().Any(m => m.Parameters.Length == 0))
+        return false;
     var dispose = nt.GetMembers("Dispose").OfType<IMethodSymbol>().FirstOrDefault(
         m => m.Parameters.Length == 0 && m.ReturnsVoid && m.TypeParameters.Length == 0);
     if (dispose is null || dispose.DeclaringSyntaxReferences.Length == 0)
 
@@ -58,6 +58,22 @@ public sealed class EmptyOverrideOverRealBase : BaseWithRealDispose
     public override void Dispose() { }   // empty, but base.Dispose does real work
 }
 
+// NON-empty cleanup via DisposeAsync, with the sync Dispose() an empty COMPATIBILITY no-op (a type
+// implementing both IDisposable and IAsyncDisposable). The empty sync body must NOT exempt it — the
+// real cleanup lives in DisposeAsync, which the flow detector treats as a release, so an undisposed
+// local still leaks (Codex P2). Name ends `Reader` so both detector paths see it.
+public sealed class AsyncReader : IDisposable, IAsyncDisposable
+{
+    private readonly System.Threading.CancellationTokenSource _cts = new();
+    public int Read() => 0;
+    public void Dispose() { }                                        // empty sync compat no-op
+    public System.Threading.Tasks.ValueTask DisposeAsync()           // REAL cleanup
+    {
+        _cts.Dispose();
+        return default;
+    }
+}
+
 public sealed class EmptyDisposeConsumers
 {
     // SILENT: an empty-Dispose enumerator local, iterated and never disposed (the ClosedXML shape).
@@ -96,4 +112,12 @@ public void LeakDerived()
         var d = new EmptyOverrideOverRealBase();
         d.Ping();                  // base.Dispose() is real -> LEAK
     }
+
+    // FLAGGED (control, Codex P2): empty SYNC Dispose but a real DisposeAsync -> never disposing
+    // (sync or async) leaks; the empty sync body must not exempt it.
+    public int LeakAsync()
+    {
+        var ar = new AsyncReader();
+        return ar.Read();          // never disposed (sync or async) -> LEAK
+    }
 }