Verification
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.
POST
/
v1
/
verify
Submit a verification
curl --request POST \
--url https://hub.theformalera.com/v1/verify \
--header 'Authorization: Bearer <token>' \
--header 'Content-Type: application/json' \
--data '
{
"schema": "theformalera.request/v1",
"kernels": [
{}
],
"specs": {},
"project": "<string>",
"lock": [
{}
]
}
'import requests
url = "https://hub.theformalera.com/v1/verify"
payload = {
"schema": "theformalera.request/v1",
"kernels": [{}],
"specs": {},
"project": "<string>",
"lock": [{}]
}
headers = {
"Authorization": "Bearer <token>",
"Content-Type": "application/json"
}
response = requests.post(url, json=payload, headers=headers)
print(response.text)const options = {
method: 'POST',
headers: {Authorization: 'Bearer <token>', 'Content-Type': 'application/json'},
body: JSON.stringify({
schema: 'theformalera.request/v1',
kernels: [{}],
specs: {},
project: '<string>',
lock: [{}]
})
};
fetch('https://hub.theformalera.com/v1/verify', options)
.then(res => res.json())
.then(res => console.log(res))
.catch(err => console.error(err));<?php
$curl = curl_init();
curl_setopt_array($curl, [
CURLOPT_URL => "https://hub.theformalera.com/v1/verify",
CURLOPT_RETURNTRANSFER => true,
CURLOPT_ENCODING => "",
CURLOPT_MAXREDIRS => 10,
CURLOPT_TIMEOUT => 30,
CURLOPT_HTTP_VERSION => CURL_HTTP_VERSION_1_1,
CURLOPT_CUSTOMREQUEST => "POST",
CURLOPT_POSTFIELDS => json_encode([
'schema' => 'theformalera.request/v1',
'kernels' => [
[
]
],
'specs' => [
],
'project' => '<string>',
'lock' => [
[
]
]
]),
CURLOPT_HTTPHEADER => [
"Authorization: Bearer <token>",
"Content-Type: application/json"
],
]);
$response = curl_exec($curl);
$err = curl_error($curl);
curl_close($curl);
if ($err) {
echo "cURL Error #:" . $err;
} else {
echo $response;
}package main
import (
"fmt"
"strings"
"net/http"
"io"
)
func main() {
url := "https://hub.theformalera.com/v1/verify"
payload := strings.NewReader("{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}")
req, _ := http.NewRequest("POST", url, payload)
req.Header.Add("Authorization", "Bearer <token>")
req.Header.Add("Content-Type", "application/json")
res, _ := http.DefaultClient.Do(req)
defer res.Body.Close()
body, _ := io.ReadAll(res.Body)
fmt.Println(string(body))
}HttpResponse<String> response = Unirest.post("https://hub.theformalera.com/v1/verify")
.header("Authorization", "Bearer <token>")
.header("Content-Type", "application/json")
.body("{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}")
.asString();require 'uri'
require 'net/http'
url = URI("https://hub.theformalera.com/v1/verify")
http = Net::HTTP.new(url.host, url.port)
http.use_ssl = true
request = Net::HTTP::Post.new(url)
request["Authorization"] = 'Bearer <token>'
request["Content-Type"] = 'application/json'
request.body = "{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}"
response = http.request(request)
puts response.read_body{
"job": "J-3f1c0a9b2d4e",
"status": "queued"
}{
"detail": "<string>"
}{
"detail": "<string>"
}{
"detail": "<string>"
}{
"detail": "<string>"
}Authorizations
A Spec Hub API token (tfe_…). The CLI reads it from THEFORMALERA_TOKEN or from theformalera login.
Body
application/json
Must be theformalera.request/v1.
Available options:
theformalera.request/v1 One entry per annotated kernel: name, file, line, lang, keys, annotation, configs (constexprs + TTIR + digest).
Verification level.
Available options:
proof, bounded, quick Resolved spec nodes, keyed by Spec Key.
Project name from theformalera.toml.
The locked spec packages (theformalera.lock entries).
⌘I
Submit a verification
curl --request POST \
--url https://hub.theformalera.com/v1/verify \
--header 'Authorization: Bearer <token>' \
--header 'Content-Type: application/json' \
--data '
{
"schema": "theformalera.request/v1",
"kernels": [
{}
],
"specs": {},
"project": "<string>",
"lock": [
{}
]
}
'import requests
url = "https://hub.theformalera.com/v1/verify"
payload = {
"schema": "theformalera.request/v1",
"kernels": [{}],
"specs": {},
"project": "<string>",
"lock": [{}]
}
headers = {
"Authorization": "Bearer <token>",
"Content-Type": "application/json"
}
response = requests.post(url, json=payload, headers=headers)
print(response.text)const options = {
method: 'POST',
headers: {Authorization: 'Bearer <token>', 'Content-Type': 'application/json'},
body: JSON.stringify({
schema: 'theformalera.request/v1',
kernels: [{}],
specs: {},
project: '<string>',
lock: [{}]
})
};
fetch('https://hub.theformalera.com/v1/verify', options)
.then(res => res.json())
.then(res => console.log(res))
.catch(err => console.error(err));<?php
$curl = curl_init();
curl_setopt_array($curl, [
CURLOPT_URL => "https://hub.theformalera.com/v1/verify",
CURLOPT_RETURNTRANSFER => true,
CURLOPT_ENCODING => "",
CURLOPT_MAXREDIRS => 10,
CURLOPT_TIMEOUT => 30,
CURLOPT_HTTP_VERSION => CURL_HTTP_VERSION_1_1,
CURLOPT_CUSTOMREQUEST => "POST",
CURLOPT_POSTFIELDS => json_encode([
'schema' => 'theformalera.request/v1',
'kernels' => [
[
]
],
'specs' => [
],
'project' => '<string>',
'lock' => [
[
]
]
]),
CURLOPT_HTTPHEADER => [
"Authorization: Bearer <token>",
"Content-Type: application/json"
],
]);
$response = curl_exec($curl);
$err = curl_error($curl);
curl_close($curl);
if ($err) {
echo "cURL Error #:" . $err;
} else {
echo $response;
}package main
import (
"fmt"
"strings"
"net/http"
"io"
)
func main() {
url := "https://hub.theformalera.com/v1/verify"
payload := strings.NewReader("{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}")
req, _ := http.NewRequest("POST", url, payload)
req.Header.Add("Authorization", "Bearer <token>")
req.Header.Add("Content-Type", "application/json")
res, _ := http.DefaultClient.Do(req)
defer res.Body.Close()
body, _ := io.ReadAll(res.Body)
fmt.Println(string(body))
}HttpResponse<String> response = Unirest.post("https://hub.theformalera.com/v1/verify")
.header("Authorization", "Bearer <token>")
.header("Content-Type", "application/json")
.body("{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}")
.asString();require 'uri'
require 'net/http'
url = URI("https://hub.theformalera.com/v1/verify")
http = Net::HTTP.new(url.host, url.port)
http.use_ssl = true
request = Net::HTTP::Post.new(url)
request["Authorization"] = 'Bearer <token>'
request["Content-Type"] = 'application/json'
request.body = "{\n \"schema\": \"theformalera.request/v1\",\n \"kernels\": [\n {}\n ],\n \"specs\": {},\n \"project\": \"<string>\",\n \"lock\": [\n {}\n ]\n}"
response = http.request(request)
puts response.read_body{
"job": "J-3f1c0a9b2d4e",
"status": "queued"
}{
"detail": "<string>"
}{
"detail": "<string>"
}{
"detail": "<string>"
}{
"detail": "<string>"
}