Continuous integration

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

.github/workflows/theformalera.yml

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

### 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.

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

.gitlab-ci.yml

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

.buildkite/pipeline.yml

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:

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 passes. --report-dir writes the JSON report, SARIF, the Markdown comment and an HTML report; see Reports.

Pre-commit

Run the quick level on the kernels staged for commit:

.pre-commit-config.yaml

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.

Get started

Concepts

Guides

Model conformance

Case studies

Help

GitHub Actions

Inputs

Outputs

The pull-request comment

GitLab CI

Buildkite

Any other CI

Pre-commit

What triggers re-verification

​GitHub Actions

​Inputs

​Outputs

​The pull-request comment

​GitLab CI

​Buildkite

​Any other CI

​Pre-commit

​What triggers re-verification

GitHub Actions

Inputs

Outputs

The pull-request comment

GitLab CI

Buildkite

Any other CI

Pre-commit

What triggers re-verification