diff --git a/README.md b/README.md
index 8533c07..c2032c0 100644
--- a/README.md
+++ b/README.md
@@ -72,6 +72,8 @@ assert repl.get_num_goals(s4) == 0
 | `Repl.get_goals(state)` | remaining goals as `Goal(hyps, ty, mvar)`, pretty-printed with Lean's real delaborator |
 | `Repl.get_num_goals(state)` | number of remaining goals |
 | `Repl.get_goal_pp(state, goal_idx=0)` | pretty-printed goal (hypotheses + `⊢ type`) |
+| `Repl.get_state_pp(state)` | pretty-print every goal of `state` in one string: `no goals` with 0 goals, exactly the `get_goal_pp(state, 0)` output for a single goal, numbered `goal[0]:\n<pp0>` blocks joined by a blank line for N goals |
+| `Goal.__str__` | standard goal display: one `name : type` line per hypothesis followed by `⊢ ty` (just `⊢ ty` with no hypotheses) — the same `hyps ⊢ type` shape as `get_goal_pp` |
 | `Repl.num_states()` | number of replay states created so far; valid ids are `0..num_states()` (half-open — highest valid id is `num_states() - 1`) |
 | `Repl.check(term, state=None, goal_idx=0)` | `#check`-style query: `"{term} : {type}"`; `state=None` checks in the root context, `state=N` in that goal's local context. A bare constant prints its declared type (as the real `#check` does, with implicit/universe arguments as binders); other terms are elaborated in the goal context |
 | `Repl.inspect(name)` | `#print`-style query: kind, type, and (for definitions/theorems/opaque constants) value, rendered by Lean's real pretty printer |
diff --git a/python/leotower/__init__.py b/python/leotower/__init__.py
index 66ad436..a31a965 100644
--- a/python/leotower/__init__.py
+++ b/python/leotower/__init__.py
@@ -17,6 +17,14 @@
 import sys
 
 from contextlib import contextmanager
+from importlib.metadata import PackageNotFoundError, version as _dist_version
+
+try:
+    __version__ = _dist_version("leotower")
+except PackageNotFoundError:
+    # No installed distribution metadata (e.g. a source checkout without
+    # `maturin develop`). Keep in sync with the version in pyproject.toml.
+    __version__ = "0.1.0"
 
 
 def _extend_windows_dll_search_path() -> None:
@@ -57,7 +65,7 @@ def _extend_windows_dll_search_path() -> None:
 
 from leotower._leotower import LeanSession, prepare_freethreaded_lean
 
-__all__ = ["with_lean", "LeanSession", "prepare_freethreaded_lean"]
+__all__ = ["__version__", "with_lean", "LeanSession", "prepare_freethreaded_lean"]
 
 
 @contextmanager
@@ -142,8 +150,12 @@ def __init__(self, module: str = "Lean"):
         top-level commands are elaborated into the session environment
         (``import`` lines are skipped).
         """
+        self._module = module
         self._repl = _Repl(module)
 
+    def __repr__(self):
+        return f"<leotower.Repl module={self._module!r}>"
+
     # -- state management ---------------------------------------------------
     def set_goal(self, type_str: str) -> int:
         """Create a new root goal state from a term string.
diff --git a/tests/test_leotower.py b/tests/test_leotower.py
index 631e9c5..fb2b57e 100644
--- a/tests/test_leotower.py
+++ b/tests/test_leotower.py
@@ -1,5 +1,8 @@
 """Smoke tests for the leotower native bindings."""
 
+import re
+from pathlib import Path
+
 import pytest
 
 import leotower
@@ -44,3 +47,14 @@ def test_repeated_sessions():
         assert lean.nat_add(1, 2) == 3
     with leotower.with_lean() as lean:
         assert lean.nat_add(2, 3) == 5
+
+
+def test_version_matches_pyproject():
+    """leotower.__version__ matches the version declared in pyproject.toml
+    (importlib.metadata when the distribution metadata is installed,
+    hardcoded fallback otherwise)."""
+    pyproject = Path(leotower.__file__).resolve().parents[2] / "pyproject.toml"
+    declared = re.search(
+        r'^version\s*=\s*"([^"]+)"', pyproject.read_text(encoding="utf-8"), re.M
+    ).group(1)
+    assert leotower.__version__ == declared
diff --git a/tests/test_repl.py b/tests/test_repl.py
index 52645b0..d034ff4 100644
--- a/tests/test_repl.py
+++ b/tests/test_repl.py
@@ -908,3 +908,21 @@ def test_every_error_is_caught_by_except_runtime_error():
     ):
         with pytest.raises(RuntimeError):
             call()
+
+
+# ---------------------------------------------------------------------------
+# Repl.__repr__
+# ---------------------------------------------------------------------------
+# Deliberately the last tests in the file: every Repl() construction
+# consumes from the shared runtime's heartbeat budget (W-407), and the
+# tactic/goal-elaboration tests above run at the edge of that budget on
+# some machines. These tests only construct — repr is pure Python — so
+# they must not run before the elaboration-heavy tests.
+
+
+def test_repr_shows_imported_module():
+    """__repr__ shows the module the session was constructed with."""
+    assert repr(Repl()) == "<leotower.Repl module='Lean'>"
+    assert repr(Repl("tests/fixtures/repl_demo.lean")) == (
+        "<leotower.Repl module='tests/fixtures/repl_demo.lean'>"
+    )