Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
alcueca wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 30 additions & 1 deletion .github/workflows/nightly-certora.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,14 +113,43 @@ jobs:
CONFIGS: ${{ matrix.configs }}
run: |
set -uo pipefail

# Certora's cloud intermittently fails to RETURN results ("request failed" /
# "Could not find job results") even when the proof itself passed ("No errors
# found by Prover!"). certoraRun then exits non-zero, reddening the nightly and
# paging Slack for a Certora-side blip, not a rule violation. Retry only those
# transient backend errors; a real violation doesn't match the pattern and fails
# fast (no wasted re-proofs).
MAX_ATTEMPTS=3
RETRY_SLEEP=60
TRANSIENT_RE='Could not find job results|request failed|An error occurred'

@greptile-apps greptile-apps Bot Aug 18, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 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


# Runs one certoraRun, streaming output live while capturing it to match on.
# Returns certoraRun's exit code; retries in place on transient cloud errors.
run_certora() {
local attempt=1 rc log
log="$(mktemp)"
while :; do
certoraRun "$@" --wait_for_results all 2>&1 | tee "$log"
rc=${PIPESTATUS[0]}
if [ "$rc" -eq 0 ]; then rm -f "$log"; return 0; fi
if [ "$attempt" -ge "$MAX_ATTEMPTS" ] || ! grep -qE "$TRANSIENT_RE" "$log"; then
rm -f "$log"; return "$rc"
fi
echo "::warning::Certora transient cloud error (attempt ${attempt}/${MAX_ATTEMPTS}), retrying in ${RETRY_SLEEP}s: $*"
attempt=$((attempt + 1))
sleep "$RETRY_SLEEP"
done
}

fail=0
while IFS= read -r line; do
# skip blank lines
[ -z "${line//[[:space:]]/}" ] && continue
# Parse the config line into args honoring quotes (no eval).
mapfile -t -d '' parts < <(printf '%s' "$line" | xargs printf '%s\0')
echo "::group::certoraRun ${parts[*]}"
if ! certoraRun "${parts[@]}" --wait_for_results all; then
if ! run_certora "${parts[@]}"; then
echo "::error::Certora verification failed for: $line"
fail=1
fi
Expand Down
Loading