Developer documentation
Build against the specification.
A key, the Python SDK, and the loop that turns one executable task definition into a training signal, a sealed evaluation, and a release decision you can hand to someone who was not in the room.
01
Get the right access
Join an existing team by invitation, or create a separate API workspace.
Ask an owner or admin for a one-time invitation link from Dashboard → Team. That joins the correct organization and workspace.
Open the dashboardUse the form below. It issues a workspace-scoped key once; it does not add you to somebody else's organization.
Store it now. We keep only a hash, so this value cannot be shown again — if it is lost we can revoke it and issue a new one, nothing more.
curl -X POST https://formalengines.com/api/signups -H 'content-type: application/json' -d '{"email":"you@example.com"}'Same endpoint, same response: 201 with the key, 409 if the email already has a workspace.
02
Install the SDK
Python 3.12 or newer. The base client is httpx, Pydantic, and the shared contracts.
pip install formal-engines --extra-index-url https://formalengines.com/pypi/simple/Wheels are served from this domain. formal-engines is not on public PyPI yet, so the extra index is required.
pip install 'formal-engines[authoring]' --extra-index-url https://formalengines.com/pypi/simple/The authoring extra adds environment packaging and local validation. It is imported only when you callspecifications.publish(path=…), as the quickstart below does.
03
Quickstart
Publish a specification, train against it, and export the release evidence.
import os
from formal_engines import FormalEngines
from formal_engines.types import Gate, ModelRef, TrainingPlan
# The client reads both of these from the environment; export them in your shell instead if you prefer.
os.environ["FORMAL_ENGINES_API_KEY"] = "fe_live_your_key"
os.environ["FORMAL_ENGINES_BASE_URL"] = "https://formalengines.com/api"
fe = FormalEngines()
# Package a local verifiers environment and publish it as an immutable specification version.
spec = fe.specifications.publish(
path="./environments/support_agent",
train_split="train",
eval_split="sealed_eval",
)
# Baseline: score the untrained model on the sealed split.
baseline = fe.evaluations.run(
specification=spec,
model=ModelRef(name="Qwen/Qwen3.5-4B"),
split="sealed_eval",
).wait()
# GRPO against the same specification that defines the reward.
training = fe.training.start(
TrainingPlan(
specification=spec,
base_model="Qwen/Qwen3.5-4B",
algorithm={"type": "grpo"},
max_steps=100,
batch_size=128,
rollouts_per_example=8,
)
)
checkpoint = training.wait().best_checkpoint
# Candidate: the trained checkpoint, scored on the split training never saw.
candidate = fe.evaluations.run(
specification=spec, model=checkpoint, split="sealed_eval"
).wait()
# Gates turn the two runs into a recorded pass or fail.
decision = fe.releases.decide(
candidate=candidate,
baseline=baseline,
gates=[
Gate.metric("task_success", minimum=0.82),
Gate.regression("policy_violation", maximum_delta=0.0),
],
)
# Signed bundle: specification version, run ids, metrics, gate results.
decision.export("release-evidence.json")publish packages the directory, creates the version, validates it, and publishes it in one call. Both run handles expose .wait(), .events(), .metrics(), and.cancel(); polling, cursors, retries, and idempotency stay inside the SDK.
04
How it works
Versions, runs, sealed splits, gates, evidence.
A specification is an executable environment — task state, tools, permitted actions, constraints, and the verifiers that decide what counts as success — published as an immutable version. Training and evaluation both address that version by id, so a reward and a score always come from the same definition of correct. Candidate checkpoints are scored on a sealed split that training never sees, which is the only thing that makes the resulting number worth quoting. Gates state the release condition as data: an absolute floor on a metric, or a no-regression bound measured against the baseline run. A release decision applies those gates to a candidate and baseline pair and freezes the outcome into an evidence bundle — specification version, run ids, metrics, gate results, and an HMAC-SHA256 signature over the canonical payload — so the record survives the argument about whether the model got better.
The product story05
API at a glance
Core runs plus trace datasets, Train and Prove workflows, and model exports.
| Resource | Purpose |
|---|---|
/v1/specifications | Create a specification, add versions, validate one, publish it. A published version is immutable and is what every run refers to. |
/v1/evaluation-runs | Score a model or checkpoint on one split of a version. Metrics and traces hang off the run. |
/v1/training-runs | Start post-training against a specification, then read metrics, logs, and checkpoints. |
/v1/runs/{run_id}/events | One server-sent event feed for both run types. Events carry a monotonic sequence, so reconnecting with the last cursor loses nothing and repeats nothing. |
/v1/release-decisions | Apply gates to a candidate and baseline pair, record the verdict, and export the evidence file. |
/v1/evidence-bundles | Retrieve the signed bundle behind a decision. |
/v1/artifacts | Content-addressed transfer of packaged environments. specifications.publish() uses it for you. |
/v1/trace-datasets | Import OpenAI-compatible agent traces, validate and sanitize them, remove duplicates, detect leakage, and freeze immutable train, validation, and sealed-evaluation splits. |
/v1/agent-improvement-workflows | Run baseline evaluation → optional SFT → GRPO → validated export → sealed candidate evaluation → release gates → signed evidence with bounded cost, cancellation, and retry. |
/v1/checkpoints/{checkpoint_id}/exports | Create a PEFT adapter or merged safetensors export. Every ready export is byte-verified, independently reloaded, and available through an expiring workspace-bound download. |
- Base URL
https://formalengines.com/api- Auth
Authorization: Bearer fe_live_…on every request. Keys are workspace-scoped.- Idempotency
- Every mutating request accepts an
Idempotency-Key. Replaying a key returns the original run instead of starting a second one.
06
Models and compute
How model resolution and automatic GPU selection work in the private beta.
You can name any public or token-accessible Hugging Face model repository. Formal Engines resolves it to an immutable commit, measures the checkpoint, and chooses a single-node 2, 4, or 8 GPU layout for separate training and inference processes. The selected type, count, and allocation appear on the run dashboard. Pods scale from zero for each run and are removed when the run ends.
This is broad, model-family-agnostic admission—not a promise that every architecture already works in the pinned Prime RL, Transformers, and vLLM runtime. Unsupported architectures fail during validation or load; models too large for one 8-GPU node are refused before dispatch. LoRA is the practical default for larger models. The shared beta keeps one concurrent Pod, an aggregate GPU ceiling, and an hourly price ceiling, so an automatically selected shape can queue or be refused instead of silently increasing spend. Your specifications, traces, and checkpoints stay in your workspace.
vatsal@formalengines.com07
Give this to your agent
One operational file with the safe workflow, commands, and evidence boundaries.
curl -fsS https://formalengines.com/SKILLS.md -o SKILLS.mdAsk the agent to read SKILLS.md before operating Formal Engines. It distinguishes team invitations from API signup, keeps credentials out of source, and requires an explicit budget before GPU work.