fix: Catch all exceptions from _run_lean to prevent UnboundLocalError (#4)

If _run_lean raises something other than TimeoutExpired (e.g.
UnicodeDecodeError from non-UTF-8 lean output), the result variable
was unbound, crashing at cache.put() and return. Now catches all
exceptions with an INCONCLUSIVE result.

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

Author: haasonsaas

formal_verification/lean_prover.py

@@ -124,6 +124,18 @@ def prove_specification(self, spec: FormalSpec) -> ProofResult:
                 prover_name="lean",
                 solver_status=ProofStatus.TIMEOUT.value,
             )
+        except Exception as exc:
+            logger.error("Lean proof attempt failed: %s", exc)
+            result = ProofResult(
+                spec=spec,
+                proven=False,
+                proof_time_ms=(time.time() - start_time) * 1000,
+                error_message=str(exc),
+                counter_example=None,
+                proof_output="",
+                prover_name="lean",
+                solver_status=ProofStatus.INCONCLUSIVE.value,
+            )
 
         if self.use_cache and self.cache:
             self.cache.put(spec, result)