fix: Don't cache timeout/error results in LeanProver (#5)

* fix: Don't cache timeout/error results in LeanProver

Only cache results from successful lean invocations (success or
type-check failure). Timeout and unexpected errors are transient and
should not permanently prevent retries for the same spec.

Matches CoqProver behavior where cache.put is inside the try block.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* fix: Move cache.put after try/except to avoid swallowing valid results

cache.put inside try was covered by the broad except Exception,
meaning a cache error would discard a valid proof result and return
INCONCLUSIVE. Since both except branches return early, cache.put
safely goes after the try/except block — only reached with a valid
result from _run_lean.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: haasonsaas

formal_verification/lean_prover.py

@@ -114,7 +114,7 @@ def prove_specification(self, spec: FormalSpec) -> ProofResult:
             result = self._run_lean(lean_code, start_time, spec)
         except subprocess.TimeoutExpired:
             logger.warning("Lean proof timeout for: %s", spec.spec_text)
-            result = ProofResult(
+            return ProofResult(
                 spec=spec,
                 proven=False,
                 proof_time_ms=self.timeout_seconds * 1000,
@@ -126,7 +126,7 @@ def prove_specification(self, spec: FormalSpec) -> ProofResult:
             )
         except Exception as exc:
             logger.error("Lean proof attempt failed: %s", exc)
-            result = ProofResult(
+            return ProofResult(
                 spec=spec,
                 proven=False,
                 proof_time_ms=(time.time() - start_time) * 1000,