diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md
index 746ee66..9a70f0d 100644
--- a/.kiro/specs/access-control-prover/tasks.md
+++ b/.kiro/specs/access-control-prover/tasks.md
@@ -144,7 +144,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
   - _Requirements: 3.1, 3.6, 11.7_
   - _Boundary: Function Summaries_
   - _Depends: 7.4, 8.3_
-- [ ] 9.2 Compute monotone summaries over recursive call components
+- [x] 9.2 Compute monotone summaries over recursive call components
   - Iterate finite summary sets over strongly connected components until stable.
   - Done when direct recursion and mutual recursion terminate with stable accumulated evidence.
   - _Requirements: 3.7, 11.6_
diff --git a/src/openultrasast/semantic/obligations/summaries.py b/src/openultrasast/semantic/obligations/summaries.py
index e84dd3b..64701df 100644
--- a/src/openultrasast/semantic/obligations/summaries.py
+++ b/src/openultrasast/semantic/obligations/summaries.py
@@ -1,13 +1,15 @@
-"""Local function summaries for the obligations abstract interpretation.
+"""Function summaries for the obligations abstract interpretation.
 
-Task 9.1 (Reqs 3.1, 3.6, 11.7). Each summary collects a function's protected
+Task 9.1 (Reqs 3.1, 3.6, 11.7): each summary collects a function's protected
 operations, local witnesses, resolved calls and local completeness WITHOUT
-traversing callers: the monotone fixpoint over strongly connected call
-components is task 9.2. Summaries are deterministic and carry no target names
-beyond fact identifiers (Req 11.7).
+traversing callers. Task 9.2 (Reqs 3.7, 11.6): a monotone fixpoint over
+strongly connected call components unions callee evidence into callers until
+stable, so direct and mutual recursion terminate with the accumulated
+evidence. Summaries are deterministic and carry no target names beyond fact
+identifiers (Req 11.7).
 """
 
-from collections.abc import Iterable, Mapping
+from collections.abc import Iterable, Iterator, Mapping
 from dataclasses import dataclass, field
 
 from ..ir import FunctionIR
@@ -87,3 +89,203 @@ def local_summaries(
                 )
             )
     return tuple(summaries)
+
+
+def _exact_caller_edges(
+    summaries_by_symbol: Mapping[SymbolId, FunctionSummary],
+) -> dict[SymbolId, tuple[SymbolId, ...]]:
+    """Caller-to-callee edges over complete single-target call sets only."""
+    edges: dict[SymbolId, tuple[SymbolId, ...]] = {}
+    for symbol, summary in summaries_by_symbol.items():
+        callees = {target for call in summary.calls if call.completeness.is_complete and len(call.targets) == 1 for target in call.targets}
+        edges[symbol] = tuple(sorted(callees))
+    return edges
+
+
+def _sorted_scc_components(
+    edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+    nodes: Iterable[SymbolId],
+) -> tuple[tuple[SymbolId, ...], ...]:
+    """Strongly connected components (members sorted, callee components first)."""
+    return _tarjan_components(edges, set(nodes))
+
+
+def _tarjan_components(edges: Mapping[SymbolId, tuple[SymbolId, ...]], known: set[SymbolId]) -> tuple[tuple[SymbolId, ...], ...]:
+    visit_index: dict[SymbolId, int] = {}
+    lowlink: dict[SymbolId, int] = {}
+    on_component_stack: set[SymbolId] = set()
+    component_stack: list[SymbolId] = []
+    components: list[tuple[SymbolId, ...]] = []
+    counter = 0
+    for root in sorted(known):
+        if root in visit_index:
+            continue
+        counter = _tarjan_visit(
+            root,
+            edges,
+            known,
+            visit_index,
+            lowlink,
+            on_component_stack,
+            component_stack,
+            components,
+            counter,
+        )
+    return tuple(components)
+
+
+def _tarjan_visit(
+    root: SymbolId,
+    edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+    known: set[SymbolId],
+    visit_index: dict[SymbolId, int],
+    lowlink: dict[SymbolId, int],
+    on_component_stack: set[SymbolId],
+    component_stack: list[SymbolId],
+    components: list[tuple[SymbolId, ...]],
+    counter: int,
+) -> int:
+    work: list[tuple[SymbolId, Iterator[SymbolId]]] = [(root, iter(edges.get(root, ())))]
+    while work:
+        node, children = work[-1]
+        if node not in visit_index:
+            visit_index[node] = counter
+            lowlink[node] = counter
+            counter += 1
+            component_stack.append(node)
+            on_component_stack.add(node)
+        descended = False
+        for child in children:
+            if child not in known:
+                continue
+            if child not in visit_index:
+                work.append((child, iter(edges.get(child, ()))))
+                descended = True
+                break
+            if child in on_component_stack:
+                lowlink[node] = min(lowlink[node], visit_index[child])
+        if descended:
+            continue
+        work.pop()
+        _tarjan_emit_component(node, lowlink, visit_index, on_component_stack, component_stack, components)
+        if work:
+            parent = work[-1][0]
+            lowlink[parent] = min(lowlink[parent], lowlink[node])
+    return counter
+
+
+def _tarjan_emit_component(
+    node: SymbolId,
+    lowlink: dict[SymbolId, int],
+    visit_index: dict[SymbolId, int],
+    on_component_stack: set[SymbolId],
+    component_stack: list[SymbolId],
+    components: list[tuple[SymbolId, ...]],
+) -> None:
+    if lowlink[node] != visit_index[node]:
+        return
+    members: list[SymbolId] = []
+    while True:
+        member = component_stack.pop()
+        on_component_stack.discard(member)
+        members.append(member)
+        if member == node:
+            break
+    components.append(tuple(sorted(members)))
+
+
+def _merge_operations(left: tuple[Operation, ...], right: tuple[Operation, ...]) -> tuple[Operation, ...]:
+    combined = set(left) | set(right)
+    return tuple(sorted(combined, key=_operation_sort_key))
+
+
+def _operation_sort_key(operation: Operation) -> tuple[str, int, str, str, str, tuple[str, ...]]:
+    return (
+        operation.path,
+        operation.line,
+        operation.function,
+        operation.kind,
+        operation.fact_id,
+        operation.requires,
+    )
+
+
+def _merge_witnesses(left: tuple[Discharge, ...], right: tuple[Discharge, ...]) -> tuple[Discharge, ...]:
+    combined = set(left) | set(right)
+    return tuple(sorted(combined, key=_witness_sort_key))
+
+
+def _witness_sort_key(discharge: Discharge) -> tuple[str, int, str, str, str, str, str]:
+    return (
+        discharge.path,
+        discharge.line if discharge.line is not None else -1,
+        discharge.function,
+        discharge.kind,
+        discharge.fact_id,
+        discharge.provenance,
+        discharge.scope,
+    )
+
+
+def _propagated(summary: FunctionSummary, callees: Iterable[FunctionSummary]) -> FunctionSummary:
+    """Union every callee's accumulated evidence into ``summary``."""
+    operations = summary.operations
+    witnesses = summary.witnesses
+    completeness = summary.completeness
+    for callee in callees:
+        operations = _merge_operations(operations, callee.operations)
+        witnesses = _merge_witnesses(witnesses, callee.witnesses)
+        completeness = join_completeness(completeness, callee.completeness)
+    return FunctionSummary(
+        symbol=summary.symbol,
+        operations=operations,
+        witnesses=witnesses,
+        calls=summary.calls,
+        completeness=completeness,
+    )
+
+
+def _stabilise_component(
+    members: tuple[FunctionSummary, ...],
+    summaries_by_symbol: dict[SymbolId, FunctionSummary],
+    edges: Mapping[SymbolId, tuple[SymbolId, ...]],
+) -> None:
+    """Iterate a component's members until every summary is stable."""
+    changed = True
+    while changed:
+        changed = False
+        for member in members:
+            current = summaries_by_symbol[member.symbol]
+            callees = [summaries_by_symbol[edge] for edge in edges.get(member.symbol, ()) if edge in summaries_by_symbol]
+            propagated = _propagated(current, callees)
+            if propagated != current:
+                summaries_by_symbol[member.symbol] = propagated
+                changed = True
+
+
+def monotone_summaries(
+    functions_by_module: Mapping[str, Iterable[FunctionIR]],
+    index: SymbolIndex,
+    *,
+    operations_by_symbol: Mapping[SymbolId, tuple[Operation, ...]] | None = None,
+    witnesses_by_symbol: Mapping[SymbolId, tuple[Discharge, ...]] | None = None,
+) -> tuple[FunctionSummary, ...]:
+    """Summaries after the monotone fixpoint over strongly connected components.
+
+    Local summaries first; then every component (callee components first) is
+    iterated until union-stable, so recursion terminates with the accumulated
+    operations, witnesses and completeness reasons of its cycle. Output order
+    matches :func:`local_summaries`.
+    """
+    local = local_summaries(
+        functions_by_module,
+        index,
+        operations_by_symbol=operations_by_symbol,
+        witnesses_by_symbol=witnesses_by_symbol,
+    )
+    summaries_by_symbol = {summary.symbol: summary for summary in local}
+    edges = _exact_caller_edges(summaries_by_symbol)
+    for component in _sorted_scc_components(edges, summaries_by_symbol):
+        members = tuple(summaries_by_symbol[member] for member in component)
+        _stabilise_component(members, summaries_by_symbol, edges)
+    return tuple(summaries_by_symbol[summary.symbol] for summary in local)
diff --git a/tests/test_obligation_summaries.py b/tests/test_obligation_summaries.py
index a95eca7..2002a0e 100644
--- a/tests/test_obligation_summaries.py
+++ b/tests/test_obligation_summaries.py
@@ -11,8 +11,8 @@ from openultrasast.semantic.ir import CallSite, FunctionIR
 from openultrasast.semantic.obligations import summaries
 from openultrasast.semantic.obligations.abstract_domain import Completeness
 from openultrasast.semantic.obligations.operations import Discharge, Operation
-from openultrasast.semantic.obligations.resolution import SymbolIndex
-from openultrasast.semantic.obligations.summaries import FunctionSummary, local_summaries
+from openultrasast.semantic.obligations.resolution import SymbolId, SymbolIndex
+from openultrasast.semantic.obligations.summaries import FunctionSummary, local_summaries, monotone_summaries
 
 PHP_CLASS = """<?php
 class InvoiceController {
@@ -43,6 +43,61 @@ class Gate {
 }
 """
 
+JAVA_SELF_LOOP = """public class Node {
+    int walk() {
+        return this.walk();
+    }
+}
+"""
+
+JAVA_MUTUAL = """public class C {
+    void a() {
+        this.b();
+    }
+    void b() {
+        this.a();
+    }
+}
+"""
+
+JAVA_CHAIN = """public class Chain {
+    void helper1() {
+        this.helper2();
+    }
+    void helper2() {
+    }
+}
+"""
+
+JAVA_THREE_CYCLE = """public class Ring {
+    void a() {
+        this.b();
+    }
+    void b() {
+        this.c();
+    }
+    void c() {
+        this.a();
+    }
+}
+"""
+
+
+def _self_call(name: str, line: int, arity: int = 0) -> CallSite:
+    return CallSite(name, line, (), (), (), False, 0, receiver="this", arity=arity)
+
+
+def _named_operation(path: str, function_name: str, resource: str) -> Operation:
+    return Operation(
+        path=path,
+        line=3,
+        function=function_name,
+        kind="protected_read",
+        fact_id="java:protected-read",
+        resource=resource,
+        requires=("path_guard",),
+    )
+
 
 def _scope_functions(fixture: str, path: str, language: str) -> tuple[FunctionIR, ...]:
     scopes = declaration_scopes(path, fixture, language)
@@ -176,3 +231,119 @@ def test_function_summary_is_frozen() -> None:
     summary = FunctionSummary.__new__(FunctionSummary)
     with pytest.raises(Exception, match="cannot assign|frozen"):
         summary.symbol = None  # type: ignore[misc,assignment]
+
+
+def _symbol_by_name(summaries: tuple[FunctionSummary, ...], name: str) -> SymbolId:
+    for summary in summaries:
+        if summary.symbol.name == name:
+            return summary.symbol
+    raise AssertionError(f"no summary named {name}")
+
+
+def test_direct_recursion_terminates_with_stable_operations() -> None:
+    index = _index((("src/Node.java", JAVA_SELF_LOOP, "java"),))
+    walk = FunctionIR("walk", (), 2, 4, (), (_self_call("walk", 3),))
+    functions = {"src/Node.java": (walk,)}
+    local = local_summaries(functions, index)
+    operations = {_symbol_by_name(local, "walk"): (_named_operation("src/Node.java", "walk", "node"),)}
+    result = monotone_summaries(functions, index, operations_by_symbol=operations)
+    assert len(result) == 1
+    assert result[0].operations == (_named_operation("src/Node.java", "walk", "node"),)
+    assert result[0].completeness == Completeness(is_complete=True)
+
+
+def test_mutual_recursion_shares_accumulated_operations_and_witnesses() -> None:
+    index = _index((("src/C.java", JAVA_MUTUAL, "java"),))
+    function_a = FunctionIR("a", (), 2, 4, (), (_self_call("b", 3),))
+    function_b = FunctionIR("b", (), 5, 7, (), (_self_call("a", 6),))
+    functions = {"src/C.java": (function_a, function_b)}
+    local = local_summaries(functions, index)
+    symbol_b = _symbol_by_name(local, "b")
+    operations = {symbol_b: (_named_operation("src/C.java", "b", "shared"),)}
+    witnesses = {symbol_b: (_witness("b"),)}
+    result = monotone_summaries(functions, index, operations_by_symbol=operations, witnesses_by_symbol=witnesses)
+    shared = (_named_operation("src/C.java", "b", "shared"),)
+    by_name = {summary.symbol.name: summary for summary in result}
+    assert by_name["a"].operations == shared
+    assert by_name["b"].operations == shared
+    assert by_name["a"].witnesses == (_witness("b"),)
+
+
+def test_chain_helper_propagates_operations_to_caller() -> None:
+    index = _index((("src/Chain.java", JAVA_CHAIN, "java"),))
+    helper1 = FunctionIR("helper1", (), 2, 4, (), (_self_call("helper2", 3),))
+    helper2 = FunctionIR("helper2", (), 5, 6, (), ())
+    functions = {"src/Chain.java": (helper1, helper2)}
+    local = local_summaries(functions, index)
+    operations = {_symbol_by_name(local, "helper2"): (_named_operation("src/Chain.java", "helper2", "chain"),)}
+    result = monotone_summaries(functions, index, operations_by_symbol=operations)
+    by_name = {summary.symbol.name: summary for summary in result}
+    assert by_name["helper1"].operations == (_named_operation("src/Chain.java", "helper2", "chain"),)
+    assert by_name["helper1"].completeness == Completeness(is_complete=True)
+
+
+def test_candidate_edges_never_propagate_operations() -> None:
+    index = _index((("src/Auditor.java", JAVA_TWO_CLASSES, "java"),))
+    review_calls = (CallSite("check", 2, (), (), (), False, 0, receiver="auditor", arity=0),)
+    review = FunctionIR("review", (), 2, 4, (), review_calls)
+    check = FunctionIR("check", (), 2, 4, (), ())
+    functions = {"src/Auditor.java": (review, check)}
+    local = local_summaries(functions, index)
+    auditor_symbol = next(symbol for symbol in (s.symbol for s in local) if symbol.enclosing_type == "Auditor")
+    operations = {auditor_symbol: (_named_operation("src/Auditor.java", "check", "auditor"),)}
+    result = monotone_summaries(functions, index, operations_by_symbol=operations)
+    by_name = {(summary.symbol.enclosing_type, summary.symbol.name): summary for summary in result}
+    assert by_name[(None, "review")].operations == ()
+    assert by_name[("Auditor", "check")].operations == (_named_operation("src/Auditor.java", "check", "auditor"),)
+
+
+def test_incomplete_callee_reason_propagates_to_caller() -> None:
+    index = _index((("src/Chain.java", JAVA_CHAIN, "java"),))
+    helper1 = FunctionIR("helper1", (), 2, 4, (), (_self_call("helper2", 3),))
+    helper2 = FunctionIR("helper2", (), 5, 6, (), (CallSite("missing", 6, (), (), (), False, 0),))
+    functions = {"src/Chain.java": (helper1, helper2)}
+    result = monotone_summaries(functions, index)
+    by_name = {summary.symbol.name: summary for summary in result}
+    assert by_name["helper2"].completeness.is_complete is False
+    assert by_name["helper1"].completeness.is_complete is False
+    assert "resolution:no_candidate" in by_name["helper1"].completeness.reasons
+
+
+def test_three_cycle_accumulates_all_operations() -> None:
+    index = _index((("src/Ring.java", JAVA_THREE_CYCLE, "java"),))
+    function_a = FunctionIR("a", (), 2, 4, (), (_self_call("b", 3),))
+    function_b = FunctionIR("b", (), 5, 7, (), (_self_call("c", 6),))
+    function_c = FunctionIR("c", (), 8, 10, (), (_self_call("a", 9),))
+    functions = {"src/Ring.java": (function_a, function_b, function_c)}
+    local = local_summaries(functions, index)
+    operations = {
+        _symbol_by_name(local, "a"): (_named_operation("src/Ring.java", "a", "ring-a"),),
+        _symbol_by_name(local, "b"): (_named_operation("src/Ring.java", "b", "ring-b"),),
+        _symbol_by_name(local, "c"): (_named_operation("src/Ring.java", "c", "ring-c"),),
+    }
+    result = monotone_summaries(functions, index, operations_by_symbol=operations)
+    accumulated = (
+        _named_operation("src/Ring.java", "a", "ring-a"),
+        _named_operation("src/Ring.java", "b", "ring-b"),
+        _named_operation("src/Ring.java", "c", "ring-c"),
+    )
+    for summary in result:
+        assert summary.operations == accumulated
+
+
+def test_monotone_summaries_are_deterministic() -> None:
+    index = _index((("src/C.java", JAVA_MUTUAL, "java"),))
+    function_a = FunctionIR("a", (), 2, 4, (), (_self_call("b", 3),))
+    function_b = FunctionIR("b", (), 5, 7, (), (_self_call("a", 6),))
+    functions = {"src/C.java": (function_a, function_b)}
+    assert monotone_summaries(functions, index) == monotone_summaries(functions, index)
+
+
+def test_monotone_output_order_matches_local_summaries() -> None:
+    index = _index((("src/C.java", JAVA_MUTUAL, "java"),))
+    function_a = FunctionIR("a", (), 2, 4, (), (_self_call("b", 3),))
+    function_b = FunctionIR("b", (), 5, 7, (), (_self_call("a", 6),))
+    functions = {"src/C.java": (function_a, function_b)}
+    assert [summary.symbol for summary in monotone_summaries(functions, index)] == [
+        summary.symbol for summary in local_summaries(functions, index)
+    ]