> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Continuous integration

> Make verification a required check on GitHub, GitLab or Buildkite, and run the quick level before every commit.

CI needs one job and no GPU runner. On pull requests, only the kernels in changed files are verified and cached results are reused. The main branch and a nightly run verify everything.

## GitHub Actions

```yaml .github/workflows/theformalera.yml theme={"system"}
name: theformalera
on:
  pull_request:
  push:
    branches: [main]
  schedule:
    - cron: "0 7 * * *"          # full nightly run; also checks spec security advisories

jobs:
  verify:
    runs-on: ubuntu-latest        # no GPU needed
    permissions:
      contents: read
      pull-requests: write        # post the PR summary comment
      security-events: write      # upload SARIF
    steps:
      - uses: actions/checkout@v4
      - uses: theformalera/verify-action@v1
        with:
          token: ${{ secrets.THEFORMALERA_TOKEN }}
          changed-only: ${{ github.event_name == 'pull_request' }}
          level: proof
          runner: cloud           # cloud | local | on-prem
          sarif: true
          comment: true
```

Then make `theformalera / verify` a required check under branch protection. A kernel that fails verification can no longer be merged.

### Inputs

| Input | Default | Meaning |
| - | - | - |
| `token` | — | Spec Hub API token |
| `changed-only` | `false` | Verify only kernels in files changed by the pull request |
| `level` | `proof` | `proof` \| `bounded` \| `quick` |
| `runner` | `cloud` | `cloud` \| `local` \| `on-prem` |
| `sarif` | `true` | Upload SARIF, so failures appear as annotations on the changed lines |
| `comment` | `true` | Post or update one summary comment on the pull request |
| `working-directory` | `.` | Directory that contains `theformalera.toml` |
| `version` | `0.9.0` | CLI version to install |
| `python-version` | `3.12` | Python used to run the CLI |

### Outputs

| Output | Meaning |
| - | - |
| `passed`, `failed`, `unknown` | Number of kernel/spec pairs per verdict |
| `report` | Path of the JSON report |
| `lemma-hits` | Lemma Hub hits of the run |
| `lemma-saved-seconds` | Estimated solver time saved |
| `lemmas-new` | New lemmas deposited |

With `runner: local`, the action installs `theformalera[triton,engine]` and caches `.theformalera/cache`, `.theformalera/lemmas/local` and the spec cache between runs. The reports and the proofs are uploaded as the `theformalera-report` artifact.

### The pull-request comment

```markdown theme={"system"}
### theformalera verify: 1 failed, 0 unknown, 5 passed

| Kernel | Spec node | Result | Detail |
| --- | --- | --- | --- |
| silu_mul_kernel | layers[*].mlp.act | PASS (PROVED) | Lean 4 proof checked |
| silu_mul_tanh_kernel | layers[*].mlp.act | PASS (PROVED) | Lean 4 proof checked |
| paged_decode_attention | layers[*].attn.core | FAILED | F-0001: wrong unless seq_len % 16 == 0 (witness B=1, seq_len=17) |
| rmsnorm_kernel | layers[*].input_norm | PASS (PROVED) | Lean 4 proof checked |
| rmsnorm_kernel | layers[*].post_attn_norm | PASS (PROVED) | Lean 4 proof checked |
| residual_add_kernel | layers[*].attn_residual | PASS (PROVED) | Lean 4 proof checked |

Model coverage Qwen/Qwen3.8-27B@1.0: 6 of 21 nodes. Full report: theformalera-report.html (artifact)
Lemma Hub: 14 hits (4 acme · 10 built-in) · ~2.3s solver time saved · 0 new
```

The SARIF upload puts the failure on `kernels/attn_decode.py:39` under **Files changed**.

> [!TIP]
>
> For CUTLASS kernels, run the job in a CUDA devel container so that `nvcc` is available. No GPU is needed: `container: nvidia/cuda:<version>-devel-ubuntu22.04`.

## GitLab CI

```yaml .gitlab-ci.yml theme={"system"}
include:
  - remote: https://hub.theformalera.com/ci/theformalera.gitlab-ci.yml
```

Set `THEFORMALERA_TOKEN` as a masked CI/CD variable. The `theformalera-verify` job runs on merge requests, on the default branch and on schedules. It publishes SARIF as a SAST report, keeps the reports and proofs as artifacts, and posts the summary to the merge request when `GITLAB_API_TOKEN` is set. Override `THEFORMALERA_LEVEL` and `THEFORMALERA_RUNNER` to change the level and run mode.

## Buildkite

```yaml .buildkite/pipeline.yml theme={"system"}
steps:
  - label: ":lock: theformalera verify"
    command: |
      pip install --quiet "theformalera[triton]==0.9.0"
      theformalera pull --no-build
      changed=""
      if [ "$BUILDKITE_PULL_REQUEST" != "false" ]; then
        changed="--changed-only origin/$BUILDKITE_PULL_REQUEST_BASE_BRANCH"
      fi
      theformalera verify --runner cloud $changed --report-dir .theformalera/report
      buildkite-agent annotate --style info --context theformalera < .theformalera/report/theformalera-comment.md || true
    artifact_paths:
      - ".theformalera/report/**/*"
      - ".theformalera/proofs/**/*"
    plugins:
      - docker#v5.11.0:
          image: "python:3.12-slim"
          propagate-environment: true
```

## Any other CI

The action is a thin wrapper around three commands:

```bash theme={"system"}
pip install "theformalera[triton]"
theformalera pull --no-build                       # --no-build: proofs are checked by the cloud runner
theformalera verify --changed-only origin/main --report-dir .theformalera/report
```

`verify` exits with status 0 only when the [policy](https://docs.theformalera.com/guides/policy-and-waivers.md) passes. `--report-dir` writes the JSON report, SARIF, the Markdown comment and an HTML report; see [Reports](https://docs.theformalera.com/reference/reports.md).

## Pre-commit

Run the quick level on the kernels staged for commit:

```yaml .pre-commit-config.yaml theme={"system"}
repos:
  - repo: https://github.com/theformalera/theformalera
    rev: v0.9.0
    hooks:
      - id: theformalera-quick     # verify --level quick on staged .py / .cu / .cuh files
      - id: theformalera-scan      # annotations parse; every kernel under require_annotation is annotated
```

## What triggers re-verification

A kernel is verified again when any of these change: its source or the `@triton.jit` helpers it calls, its annotation, the locked spec version, the engine version, or the relevant settings in `theformalera.toml`. Comments and formatting do not change the lowered IR, so they do not trigger a new proof.

On the nightly run, UNKNOWN results are retried when new lemmas for their node have appeared, and spec security advisories for the locked versions are reported.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.