ci(certora): retry transient Certora cloud errors in nightly

[alcueca]

Problem

nightly-certora intermittently reddens (and pages Slack) when Certora's cloud fails to return results — certoraRun prints ERROR: request failed / Could not find job results and exits non-zero even though the proof itself passed (No errors found by Prover!). At the run level this is indistinguishable from a real rule violation.

Observed on unchanged commit 39f9d31 (which passed on adjacent nights):

• 2026-08-05 — all 10 jobs hit it
• 2026-08-07 — 1 job (main / C), with No errors found by Prover! right above the retrieval error

Fix

Wrap certoraRun in a retry that fires only on the transient retrieval errors (matched by pattern), up to 3 attempts with 60s backoff:

• Transient cloud blip → retry (a single retry has cleared it in every manual re-run).
• Real rule violation → doesn't match the pattern, fails fast — no wasted re-proofs, no masking.
• Persistent outage → still fails after 3 attempts, so genuine problems still page.
• Output streamed live (tee) while captured for matching — CI logs unchanged.

Validated: YAML parses, bash -n clean, and a behavioral harness confirmed transient→3 attempts/fail, violation→1 attempt/fail-fast, success→1 attempt. +30/-1, one call site changed (run_certora wraps the direct call).

🤖 Generated with Claude Code

[greptile-apps]

Greptile Summary

The PR adds bounded retries around nightly Certora runs to tolerate known cloud result-retrieval failures while preserving synchronous verdict handling.

• Streams each attempt through tee and captures the original certoraRun status.
• Retries matching failures up to three times with a 60-second backoff.
• Keeps nonmatching and exhausted failures visible to the existing workflow failure handling.

Confidence Score: 4/5

The PR appears safe to merge, with a non-blocking recommendation to narrow the transient-error pattern so unrelated failures still fail fast.

The retry remains bounded and ultimately propagates the original nonzero Certora status, but the generic An error occurred match can unnecessarily rerun persistent non-retrieval failures.

Files Needing Attention: .github/workflows/nightly-certora.yml

Important Files Changed

Filename	Overview
.github/workflows/nightly-certora.yml	Adds sound bounded retry and status propagation, but one generic regex alternative can classify unrelated Certora errors as transient.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Run certoraRun and capture output] --> B{Exit code zero?}
    B -->|Yes| C[Return success]
    B -->|No| D{Attempts exhausted or no regex match?}
    D -->|Yes| E[Return certoraRun failure]
    D -->|No| F[Wait 60 seconds]
    F --> A

Loading

_{Reviews (1): Last reviewed commit: "ci(certora): retry transient Certora clo..." | Re-trigger Greptile}

[greptile-apps]

Overbroad transient-error pattern

If a non-transient Certora configuration, compilation, or internal failure emits An error occurred, this generic alternative classifies it as transient and resubmits the complete proof up to two additional times, delaying the nightly failure notification. Restricting the pattern to known result-retrieval errors keeps substantive failures on the intended fail-fast path.

Suggested change

	TRANSIENT_RE='Could not find job results|request failed|An error occurred'
	TRANSIENT_RE='Could not find job results|request failed'

Knowledge Base Used: CI, Testing, and Fuzzing