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

# Submit a verification

> Queue a verification request (`theformalera.request/v1`) for the cloud solve workers. The request carries the lowered Triton IR of every constexpr configuration, the annotations and the resolved spec nodes; never the repository. Poll the returned job with `GET /v1/jobs/{job_id}`. Requests are limited to 64 MiB and count against the tenant's quota.



## OpenAPI

````yaml /api-reference/openapi.json post /v1/verify
openapi: 3.1.0
info:
  title: Spec Hub API
  version: '1'
  description: >-
    The registry of Lean 4 specification packages, the cloud verification queue
    and the Lemma Hub. The `theformalera` CLI is the main client; this API is
    what it calls.
servers:
  - url: https://hub.theformalera.com
    description: Spec Hub
  - url: http://127.0.0.1:8700
    description: Local Hub (`theformalera-hub serve`)
security: []
tags:
  - name: Registry
    description: 'Public: no token needed.'
  - name: Verification
    description: Cloud solving (`runner = "cloud"`).
  - name: Lemma Hub
    description: Lemma retrieval, deposit and usage statistics.
paths:
  /v1/verify:
    post:
      tags:
        - Verification
      summary: Submit a verification
      description: >-
        Queue a verification request (`theformalera.request/v1`) for the cloud
        solve workers. The request carries the lowered Triton IR of every
        constexpr configuration, the annotations and the resolved spec nodes;
        never the repository. Poll the returned job with `GET
        /v1/jobs/{job_id}`. Requests are limited to 64 MiB and count against the
        tenant's quota.
      operationId: verify_v1_verify_post
      parameters: []
      requestBody:
        required: true
        content:
          application/json:
            schema:
              type: object
              properties:
                schema:
                  type: string
                  description: Must be `theformalera.request/v1`.
                  enum:
                    - theformalera.request/v1
                level:
                  type: string
                  description: Verification level.
                  enum:
                    - proof
                    - bounded
                    - quick
                kernels:
                  type: array
                  items:
                    type: object
                    properties: {}
                  description: >-
                    One entry per annotated kernel: name, file, line, lang,
                    keys, annotation, configs (constexprs + TTIR + digest).
                specs:
                  type: object
                  properties: {}
                  description: Resolved spec nodes, keyed by Spec Key.
                project:
                  type: string
                  description: Project name from `theformalera.toml`.
                lock:
                  type: array
                  items:
                    type: object
                    properties: {}
                  description: The locked spec packages (`theformalera.lock` entries).
              required:
                - schema
                - kernels
      responses:
        '202':
          description: Accepted.
          content:
            application/json:
              schema:
                type: object
                properties:
                  job:
                    type: string
                    description: Job id.
                    example: J-3f1c0a9b2d4e
                  status:
                    type: string
                    description: Always `queued`.
              example:
                job: J-3f1c0a9b2d4e
                status: queued
        '400':
          description: Invalid JSON or wrong schema.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '401':
          description: Missing or invalid bearer token.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '402':
          description: Cloud verification quota exhausted.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
        '413':
          description: Request larger than 64 MiB.
          content:
            application/json:
              schema:
                $ref: '#/components/schemas/Error'
      security:
        - bearerAuth: []
components:
  schemas:
    Error:
      type: object
      properties:
        detail:
          type: string
          description: Why the request was refused.
      required:
        - detail
  securitySchemes:
    bearerAuth:
      type: http
      scheme: bearer
      description: >-
        A Spec Hub API token (`tfe_…`). The CLI reads it from
        `THEFORMALERA_TOKEN` or from `theformalera login`.

````

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