← Front page · Continuous Integration & Badges

GitHub Actions · Pull-Request Gate

Run SeamCert on every pull request

Gate your repository’s statement file in GitHub Actions so a pull request that introduces a sorry, custom axiom, unapproved native_decide, or contradictory hypothesis fails CI immediately—and publish a live specification-seam badge in your README.md.

1. Add the GitHub Actions workflow

Save the workflow below as .github/workflows/seamcert.yml and replace Main.lean with the path to your challenge or main theorem file. No API key or registration is required (rate-limited to 30 scans per hour per runner IP).

Copy workflow YAML

name: SeamCert Statement Check
on:
  pull_request:
    paths:
      - '**.lean'
  push:
    branches: [main]

jobs:
  seamcert:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Scan main Lean 4 statement file
        run: |
          # Replace Main.lean with the file that states your main theorems
          FILE="Main.lean"
          RESP=$(curl -fsSL -X POST https://seamcert.com/api/ci-scan \
            -F "name=${FILE}" \
            -F "source=@${FILE}" \
            -F "fail_on=high")
          echo "$RESP" | jq .
          URL=$(echo "$RESP" | jq -r .report_url)
          Badge=$(echo "$RESP" | jq -r .badge_markdown)
          echo "### SeamCert Statement Report" >> "$GITHUB_STEP_SUMMARY"
          echo "- Report: ${URL}" >> "$GITHUB_STEP_SUMMARY"
          echo "- Badge: \`${Badge}\`" >> "$GITHUB_STEP_SUMMARY"
          test "$(echo "$RESP" | jq -r .passed)" = "true"

name: SeamCert Statement Check on: pull_request: paths: - '**.lean' push: branches: [main] jobs: seamcert: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - name: Scan main Lean 4 statement file run: | # Replace Main.lean with the file that states your main theorems FILE="Main.lean" RESP=$(curl -fsSL -X POST https://seamcert.com/api/ci-scan \ -F "name=${FILE}" \ -F "source=@${FILE}" \ -F "fail_on=high") echo "$RESP" | jq . URL=$(echo "$RESP" | jq -r .report_url) Badge=$(echo "$RESP" | jq -r .badge_markdown) echo "### SeamCert Statement Report" >> "$GITHUB_STEP_SUMMARY" echo "- Report: ${URL}" >> "$GITHUB_STEP_SUMMARY" echo "- Badge: \`${Badge}\`" >> "$GITHUB_STEP_SUMMARY" test "$(echo "$RESP" | jq -r .passed)" = "true"

2. How POST /api/ci-scan works

• Endpoint: POST https://seamcert.com/api/ci-scan (multipart form or URL-encoded: source, optional name, optional fail_on=critical|high|elevated|never, default high).
• JSON response: Returns passed (boolean), risk (0–100), level (low, elevated, high), counts by severity, report_url, mutants_url (downloadable Mutants.lean to compile in your Lake step), badge_url, and badge_markdown.
• Privacy: Just like the web scanner, nothing is compiled or executed on our server and the source file itself is not stored—only the 30-day unlisted report.