Prove redesign

README.md

@@ -7,6 +7,7 @@ Point it at a Lean file or project and it inspects diagnostics and goals, edits
 ```bash
 leanflow                          # interactive shell
 leanflow workflow prove Main.lean # or run a workflow directly
+leanflow workflow prove Main.lean --provider codex --research
 ```
 
 ## Features
@@ -82,8 +83,20 @@ LeanFlow reaches that by working in small, Lean-verified steps rather than one b
 
 - **`prove <file>`** drives the model one declaration at a time, re-checking with Lean after every edit and advancing only when the target is clean. Failed attempts are recorded and the original `sorry` is restored, so the file always stays buildable.
 - **`prove`** (no file) scans the project for remaining `sorry`s, ranks the files, and works them one at a time. Parallel agents stay off unless you opt into swarm mode.
+- **`prove --research`** keeps the foreground prover moving while two process-isolated research
+  workers explore grounding and alternate routes. That worker count is also the shared live-actor
+  cap for process jobs and in-process planner lanes, so a planner wave cannot silently add three
+  more resident conversations. Rejected turns receive a non-authoritative persistence coach, and
+  cycle/route ceilings roll durable campaign epochs instead of stopping. Foreground `lean-lsp`
+  stays enabled, but its additional multi-gigabyte local Loogle index is off for this profile;
+  set `LEANFLOW_RESEARCH_LOCAL_LOOGLE=1` only for a memory-provisioned campaign.
 - **`formalize` / `autoformalize`** turn a LaTeX/PDF source into a buildable Lean draft with source-linked statements and intentional `sorry`s. The draft is handed off once it builds and its statement/source review is approved; you then run `/prove` to fill in the proofs.
 
+Headless proof outcomes are explicit: `0` means verified, `3` means an authoritatively promoted
+main-goal disproof, `2` means unresolved but checkpointed/resumable, `1` is a startup/runtime
+failure, and `130` is a signal interruption. LeanFlow never returns success while the requested
+scope still contains `sorry`.
+
 The deeper mechanics (LaTeX preflight, the blueprint/verifier handoff, the project prove-manager, queue and checkpoint internals) are in the [product reference](docs/product-reference.md).
 
 ## Workflows
@@ -92,7 +105,6 @@ The deeper mechanics (LaTeX preflight, the blueprint/verifier handoff, the proje
 - `formalize` — turn a LaTeX/PDF source document or TeX project into statement-verified Lean declarations; `/prove` then fills the resulting `sorry`s.
 - `draft` — create Lean declarations and proof skeletons.
 - `review` — inspect blockers, diagnostics, goals, and remaining `sorry`.
-- `checkpoint` — summarize workflow state for resume or handoff.
 - `refactor` / `golf` — simplify existing Lean code without breaking verification.
 
 `autoprove` and `autoformalize` are compatibility aliases of `prove` and `formalize`.
@@ -167,7 +179,11 @@ LeanFlow keeps user-level state separate from per-project workflow state:
 - project manifest: `.leanflow/project.yaml`  ·  project workflow state: `.leanflow/workflow-state/`
 
 Workflow state holds activity, logs, checkpoints, file locks, route decisions, failed-attempt
-history, project prove-manager plans, and outcomes — this is what lets long Lean runs resume.
+history, provider-turn identities, project prove-manager plans, and outcomes — this is what lets
+long Lean runs resume. Provider/infrastructure pauses take a final deterministic source checkpoint
+before exit, including edits made immediately before the provider became unavailable. Transient
+provider failures receive three interruptible retries after 5, 15, and 45 seconds; only exhaustion
+of that full recovery window produces the resumable exit-`2` pause.
 
 ## Skills and specs
 

agent/accounting/error_log.py

@@ -0,0 +1,105 @@
+"""Configure the optional process-wide LeanFlow error log.
+
+The active home is resolved for every agent construction because CLI and test
+processes may change ``LEANFLOW_HOME`` after :mod:`run_agent` is imported.
+Handler installation is process-global, so this module serializes replacement
+and marks only handlers it owns for retirement on a later home change.
+"""
+
+from __future__ import annotations
+
+import logging
+import threading
+from logging.handlers import RotatingFileHandler
+from pathlib import Path
+
+from agent.accounting.redact import RedactingFormatter
+from core.home import leanflow_home
+
+_ERROR_HANDLER_LOCK = threading.RLock()
+_LEANFLOW_OWNED_ATTR = "_leanflow_owned_error_log_handler"
+_ERROR_LOG_FORMAT = "%(asctime)s %(levelname)s %(name)s: %(message)s"
+_ERROR_LOG_MAX_BYTES = 2 * 1024 * 1024
+_ERROR_LOG_BACKUP_COUNT = 2
+
+
+def _handler_path(handler: logging.Handler) -> Path | None:
+    """Return one file handler's resolved destination when available."""
+    raw_path = getattr(handler, "baseFilename", None)
+    if not isinstance(raw_path, str) or not raw_path:
+        return None
+    try:
+        return Path(raw_path).resolve()
+    except (OSError, RuntimeError):
+        return None
+
+
+def _retire_owned_handlers(
+    target_logger: logging.Logger,
+    *,
+    keep: logging.Handler | None,
+) -> None:
+    """Remove and close stale handlers created by this module only."""
+    for handler in tuple(target_logger.handlers):
+        if handler is keep or not bool(getattr(handler, _LEANFLOW_OWNED_ATTR, False)):
+            continue
+        target_logger.removeHandler(handler)
+        try:
+            handler.close()
+        except OSError:
+            pass
+
+
+def ensure_error_log_handler(
+    target_logger: logging.Logger | None = None,
+) -> logging.Handler | None:
+    """Install or reuse the optional handler for the current LeanFlow home.
+
+    A home change retires only handlers previously installed here; unrelated
+    application handlers remain untouched. Filesystem failures disable this
+    optional sink without preventing agent construction.
+    """
+    active_logger = target_logger if target_logger is not None else logging.getLogger()
+    try:
+        error_log_path = (leanflow_home() / "logs" / "errors.log").resolve()
+    except (OSError, RuntimeError):
+        return None
+
+    with _ERROR_HANDLER_LOCK:
+        matching_handler = next(
+            (
+                handler
+                for handler in active_logger.handlers
+                if _handler_path(handler) == error_log_path
+            ),
+            None,
+        )
+        if matching_handler is not None:
+            _retire_owned_handlers(active_logger, keep=matching_handler)
+            return matching_handler
+
+        error_file_handler: RotatingFileHandler | None = None
+        try:
+            error_log_path.parent.mkdir(parents=True, exist_ok=True)
+            error_file_handler = RotatingFileHandler(
+                error_log_path,
+                maxBytes=_ERROR_LOG_MAX_BYTES,
+                backupCount=_ERROR_LOG_BACKUP_COUNT,
+            )
+            error_file_handler.setLevel(logging.WARNING)
+            error_file_handler.setFormatter(RedactingFormatter(_ERROR_LOG_FORMAT))
+            setattr(error_file_handler, _LEANFLOW_OWNED_ATTR, True)
+            active_logger.addHandler(error_file_handler)
+        except OSError:
+            if error_file_handler is not None:
+                try:
+                    error_file_handler.close()
+                except OSError:
+                    pass
+            # Never keep writing an owned optional log into a previous home
+            # after the runtime home authority has changed.
+            _retire_owned_handlers(active_logger, keep=None)
+            return None
+
+        _retire_owned_handlers(active_logger, keep=error_file_handler)
+        return error_file_handler

agent/accounting/redact.py

@@ -3,13 +3,14 @@
 Applies pattern matching to mask API keys, tokens, and credentials
 before they reach log files, verbose output, or gateway logs.
 
-Short tokens (< 18 chars) are fully masked. Longer tokens preserve
-the first 6 and last 4 characters for debuggability.
+All matched credential values are fully masked. Prefixes and suffixes remain
+credential material and therefore never survive redaction.
 """
 
 import logging
 import os
 import re
+from typing import Any, Sequence
 
 logger = logging.getLogger(__name__)
 
@@ -83,13 +84,17 @@
 
 # Compile known prefix patterns into one alternation
 _PREFIX_RE = re.compile(r"(?<![A-Za-z0-9_-])(" + "|".join(_PREFIX_PATTERNS) + r")(?![A-Za-z0-9_-])")
+_JWT_CREDENTIAL_RE = re.compile(
+    r"(?<![A-Za-z0-9_-])(?<![A-Za-z0-9_-]\.)"
+    r"eyJ[A-Za-z0-9_-]{13,}\.[A-Za-z0-9_-]{16,}\.[A-Za-z0-9_-]{16,}"
+    r"(?![A-Za-z0-9_-])(?!\.[A-Za-z0-9_-])"
+)
 
 
 def _mask_token(token: str) -> str:
-    """Mask a token, preserving prefix for long tokens."""
-    if len(token) < 18:
-        return "***"
-    return f"{token[:6]}...{token[-4:]}"
+    """Mask a token without retaining any credential-derived text."""
+    del token
+    return "***"
 
 
 def redact_sensitive_text(text: str) -> str:
@@ -103,6 +108,9 @@ def redact_sensitive_text(text: str) -> str:
     if os.getenv("LEANFLOW_REDACT_SECRETS", "").lower() in ("0", "false", "no", "off"):
         return text
 
+    # Raw JWTs may arrive without an Authorization or named-field label.
+    text = _JWT_CREDENTIAL_RE.sub("***", text)
+
     # Known prefixes (sk-, ghp_, etc.)
     text = _PREFIX_RE.sub(lambda m: _mask_token(m.group(1)), text)
 
@@ -126,13 +134,8 @@ def _redact_json(m):
         text,
     )
 
-    # Telegram bot tokens
-    def _redact_telegram(m):
-        prefix = m.group(1) or ""
-        digits = m.group(2)
-        return f"{prefix}{digits}:***"
-
-    text = _TELEGRAM_RE.sub(_redact_telegram, text)
+    # Telegram bot tokens are single credentials; retain no bot-id prefix.
+    text = _TELEGRAM_RE.sub("[REDACTED]", text)
 
     # Private key blocks
     text = _PRIVATE_KEY_RE.sub("[REDACTED PRIVATE KEY]", text)
@@ -152,6 +155,34 @@ def _redact_phone(m):
     return text
 
 
+def redact_sensitive_value(
+    value: Any,
+    *,
+    exact_secrets: Sequence[str] = (),
+) -> Any:
+    """Recursively redact structured log data and exact caller-owned secrets.
+
+    Exact-secret replacement is unconditional so a credential explicitly owned
+    by the caller cannot leak even when optional pattern redaction is disabled.
+    """
+    secrets = tuple(secret for secret in exact_secrets if isinstance(secret, str) and secret)
+    if isinstance(value, str):
+        for secret in secrets:
+            value = value.replace(secret, "[REDACTED]")
+        return redact_sensitive_text(value)
+    if isinstance(value, dict):
+        return {
+            key: redact_sensitive_value(item, exact_secrets=secrets) for key, item in value.items()
+        }
+    if isinstance(value, list):
+        return [redact_sensitive_value(item, exact_secrets=secrets) for item in value]
+    if isinstance(value, tuple):
+        return tuple(redact_sensitive_value(item, exact_secrets=secrets) for item in value)
+    if value is None or isinstance(value, (bool, int, float)):
+        return value
+    return redact_sensitive_value(str(value), exact_secrets=secrets)
+
+
 class RedactingFormatter(logging.Formatter):
     """Log formatter that redacts secrets from all log messages."""