diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md
index a29ea01..746ee66 100644
--- a/.kiro/specs/access-control-prover/tasks.md
+++ b/.kiro/specs/access-control-prover/tasks.md
@@ -138,7 +138,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
   - _Depends: 8.2, 8.3_
 
 - [ ] 9. Interprocedural summaries and concrete paths
-- [ ] 9.1 Extract local function summaries
+- [x] 9.1 Extract local function summaries
   - Collect each function's operations, witnesses, resolved calls and local completeness without traversing callers.
   - Done when summaries are deterministic and contain no target names outside fact identifiers.
   - _Requirements: 3.1, 3.6, 11.7_
diff --git a/src/openultrasast/semantic/obligations/summaries.py b/src/openultrasast/semantic/obligations/summaries.py
new file mode 100644
index 0000000..e84dd3b
--- /dev/null
+++ b/src/openultrasast/semantic/obligations/summaries.py
@@ -0,0 +1,89 @@
+"""Local function summaries for the obligations abstract interpretation.
+
+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).
+"""
+
+from collections.abc import Iterable, Mapping
+from dataclasses import dataclass, field
+
+from ..ir import FunctionIR
+from .abstract_domain import Completeness, join_completeness
+from .operations import Discharge, Operation
+from .resolution import CallTargetSet, SymbolId, SymbolIndex, resolve_call
+
+
+@dataclass(frozen=True)
+class FunctionSummary:
+    """Local summary of one function: what it holds, whom it calls."""
+
+    symbol: SymbolId
+    operations: tuple[Operation, ...] = ()
+    witnesses: tuple[Discharge, ...] = ()
+    calls: tuple[CallTargetSet, ...] = ()
+    completeness: Completeness = field(default_factory=lambda: Completeness(is_complete=True))
+
+
+def _enclosing_type(index: SymbolIndex, module: str, name: str) -> str | None:
+    """Return the enclosing type of the function ``name`` declared in ``module``."""
+    for symbol in index.by_name.get(name, ()):
+        if symbol.module == module:
+            return symbol.enclosing_type
+    return None
+
+
+def _function_symbol(index: SymbolIndex, module: str, function_ir: FunctionIR) -> SymbolId:
+    """Build the stable identity of ``function_ir`` within ``module``."""
+    enclosing_type = _enclosing_type(index, module, function_ir.name)
+    signature = tuple(function_ir.params) if function_ir.params else None
+    return SymbolId(module, enclosing_type, function_ir.name, signature)
+
+
+def _joined_call_completeness(calls: tuple[CallTargetSet, ...]) -> Completeness:
+    """Join the completeness of every resolved call into one local value."""
+    completeness = Completeness(is_complete=True)
+    for call in calls:
+        completeness = join_completeness(completeness, call.completeness)
+    return completeness
+
+
+def _sorted_functions(functions: Iterable[FunctionIR]) -> tuple[FunctionIR, ...]:
+    """Deterministic function order (name, start line)."""
+    return tuple(sorted(functions, key=lambda fn: (fn.name, fn.start_line)))
+
+
+def local_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, ...]:
+    """Summarise every function locally: operations, witnesses, resolved calls.
+
+    No caller traversal happens here (task 9.2 owns the monotone fixpoint);
+    completeness joins only the resolution completeness of the function's own
+    calls plus the injected operation/witness completeness, so an unresolved or
+    ambiguous call leaves the summary incomplete with its reason preserved.
+    """
+    operations_by_symbol = operations_by_symbol or {}
+    witnesses_by_symbol = witnesses_by_symbol or {}
+    summaries: list[FunctionSummary] = []
+    for module in sorted(functions_by_module):
+        for function_ir in _sorted_functions(functions_by_module[module]):
+            symbol = _function_symbol(index, module, function_ir)
+            calls = tuple(resolve_call(call, module=module, index=index) for call in function_ir.calls)
+            completeness = _joined_call_completeness(calls)
+            summaries.append(
+                FunctionSummary(
+                    symbol=symbol,
+                    operations=operations_by_symbol.get(symbol, ()),
+                    witnesses=witnesses_by_symbol.get(symbol, ()),
+                    calls=calls,
+                    completeness=completeness,
+                )
+            )
+    return tuple(summaries)
diff --git a/tests/test_obligation_summaries.py b/tests/test_obligation_summaries.py
new file mode 100644
index 0000000..a95eca7
--- /dev/null
+++ b/tests/test_obligation_summaries.py
@@ -0,0 +1,178 @@
+"""Task 9.1 -- local function summaries: determinism, no caller traversal."""
+
+from __future__ import annotations
+
+import inspect
+
+import pytest
+
+from openultrasast.semantic.cst import declaration_scopes
+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
+
+PHP_CLASS = """<?php
+class InvoiceController {
+    public function preview($fields) {
+        return $this->render($fields);
+    }
+}
+"""
+
+JAVA_ONE_CLASS = """public class Handler {
+    public void handle() {
+        this.run();
+    }
+    void run() {
+    }
+}
+"""
+
+JAVA_TWO_CLASSES = """public class Auditor {
+    public boolean check() {
+        return true;
+    }
+}
+class Gate {
+    public boolean check() {
+        return false;
+    }
+}
+"""
+
+
+def _scope_functions(fixture: str, path: str, language: str) -> tuple[FunctionIR, ...]:
+    scopes = declaration_scopes(path, fixture, language)
+    assert scopes, f"fixture produced no declaration scopes: {path}"
+    functions = []
+    for scope in scopes:
+        calls = (CallSite("render", 4, (), (), (), False, 0),) if scope.function_name == "preview" else ()
+        functions.append(
+            FunctionIR(
+                name=scope.function_name,
+                params=scope.params,
+                start_line=scope.start_line,
+                end_line=scope.start_line + 3,
+                binds=(),
+                calls=calls,
+            )
+        )
+    return tuple(functions)
+
+
+def _index(fixtures: tuple[tuple[str, str, str], ...]) -> SymbolIndex:
+    return SymbolIndex.build(fixtures)
+
+
+def _operation(function_name: str) -> Operation:
+    return Operation(
+        path="src/InvoiceController.php",
+        line=3,
+        function=function_name,
+        kind="protected_read",
+        fact_id="php:protected-read",
+        resource="invoice",
+        requires=("path_guard",),
+    )
+
+
+def _witness(function_name: str) -> Discharge:
+    return Discharge(
+        path="src/InvoiceController.php",
+        line=2,
+        function=function_name,
+        kind="path_guard",
+        fact_id="php:authorize",
+        provenance="call",
+        scope="statement",
+        detail="authorize",
+    )
+
+
+def test_empty_function_produces_a_complete_empty_summary() -> None:
+    index = _index((("src/Handler.java", JAVA_ONE_CLASS, "java"),))
+    functions = {"src/Handler.java": (FunctionIR("run", (), 7, 8, (), ()),)}
+    (summary,) = local_summaries(functions, index)
+    assert summary.symbol.name == "run"
+    assert summary.operations == ()
+    assert summary.witnesses == ()
+    assert summary.calls == ()
+    assert summary.completeness == Completeness(is_complete=True)
+
+
+def test_unresolved_call_leaves_local_completeness_incomplete() -> None:
+    index = _index((("src/Handler.java", JAVA_ONE_CLASS, "java"),))
+    calls = (CallSite("missing", 3, (), (), (), False, 0),)
+    functions = {"src/Handler.java": (FunctionIR("handle", (), 2, 5, (), calls),)}
+    (summary,) = local_summaries(functions, index)
+    assert summary.completeness.is_complete is False
+    assert "resolution:no_candidate" in summary.completeness.reasons
+
+
+def test_variable_receiver_call_stays_incomplete() -> None:
+    index = _index((("src/Auditor.java", JAVA_TWO_CLASSES, "java"),))
+    calls = (CallSite("check", 2, (), (), (), False, 0, receiver="auditor", arity=0),)
+    functions = {"src/Auditor.java": (FunctionIR("review", (), 2, 4, (), calls),)}
+    (summary,) = local_summaries(functions, index)
+    assert len(summary.calls[0].targets) == 2
+    assert summary.completeness.is_complete is False
+    assert "resolution:receiver_type_unknown" in summary.completeness.reasons
+
+
+def test_exact_self_call_is_complete() -> None:
+    index = _index((("src/Handler.java", JAVA_ONE_CLASS, "java"),))
+    calls = (CallSite("run", 3, (), (), (), False, 0, receiver="this", arity=0),)
+    functions = {"src/Handler.java": (FunctionIR("handle", (), 2, 5, (), calls),)}
+    (summary,) = local_summaries(functions, index)
+    assert len(summary.calls[0].targets) == 1
+    assert summary.completeness == Completeness(is_complete=True)
+
+
+def test_injected_operations_and_witnesses_are_preserved() -> None:
+    index = _index((("src/InvoiceController.php", PHP_CLASS, "php"),))
+    scopes = declaration_scopes("src/InvoiceController.php", PHP_CLASS, "php")
+    preview_scope = scopes[0]
+    functions = {"src/InvoiceController.php": (FunctionIR(preview_scope.function_name, preview_scope.params, 3, 5, (), ()),)}
+    symbol = local_summaries(functions, index)[0].symbol
+    operations = {symbol: (_operation(preview_scope.function_name),)}
+    witnesses = {symbol: (_witness(preview_scope.function_name),)}
+    (summary,) = local_summaries(functions, index, operations_by_symbol=operations, witnesses_by_symbol=witnesses)
+    assert summary.operations == (_operation(preview_scope.function_name),)
+    assert summary.witnesses == (_witness(preview_scope.function_name),)
+
+
+def test_summary_symbol_carries_enclosing_type_and_signature() -> None:
+    index = _index((("src/InvoiceController.php", PHP_CLASS, "php"),))
+    functions = {"src/InvoiceController.php": (FunctionIR("preview", ("$fields",), 3, 5, (), ()),)}
+    (summary,) = local_summaries(functions, index)
+    assert summary.symbol.enclosing_type == "InvoiceController"
+    assert summary.symbol.signature == ("$fields",)
+
+
+def test_summaries_are_deterministic_across_builds() -> None:
+    index = _index(
+        (
+            ("src/InvoiceController.php", PHP_CLASS, "php"),
+            ("src/Handler.java", JAVA_ONE_CLASS, "java"),
+        )
+    )
+    functions = {
+        "src/Handler.java": (FunctionIR("handle", (), 2, 5, (), ()),),
+        "src/InvoiceController.php": (FunctionIR("preview", ("$fields",), 3, 5, (), ()),),
+    }
+    assert local_summaries(functions, index) == local_summaries(functions, index)
+
+
+def test_module_text_contains_no_target_names() -> None:
+    module_source = inspect.getsource(summaries)
+    for target_name in ("symfony", "laravel", "tornado", "wordpress", "stapler", "jetty", "rails", "spring"):
+        assert target_name not in module_source.lower()
+
+
+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]