---
name: use-formal-engines
description: Use the live Formal Engines dashboard, Python SDK, and executable-specification workflow. Apply when joining a Formal Engines organization, inspecting runs, publishing a verifiers environment, launching approved post-training or evaluation work, retrieving checkpoints, or exporting release evidence.
---

# Use Formal Engines

Formal Engines is a post-training control plane. It turns one versioned executable task
specification into training rewards, sealed evaluations, release gates, and durable evidence.
It is not a model host or a generic trainer.

## Start at the correct surface

- Product: <https://formalengines.com/>
- Public read-only demo: <https://formalengines.com/demo/>
- Team dashboard: <https://formalengines.com/dashboard/>
- Developer documentation: <https://formalengines.com/docs/>
- API base URL: `https://formalengines.com/api`

Use the public demo when someone only needs to inspect the product. Use a dashboard invitation
when they must join an existing organization. Use API signup only when they intentionally want
a separate workspace.

## Join an existing team

1. Ask an organization owner or admin to open **Dashboard → Team**.
2. Have them choose the least-privileged role that fits:
   - `viewer`: inspect organization data; cannot mutate workspace data.
   - `member`: run normal workspace operations.
   - `admin`: administer members and API keys as well as workspace operations.
   - `owner`: full organization control; only an owner can create or manage another owner.
3. Open the one-time invitation link they send. The token lives in the URL fragment and is not
   sent in an HTTP request before acceptance.
4. Create a unique password of at least 12 characters and store it in a password manager.
5. Sign in at the dashboard. Never share a dashboard password or browser session with an agent.

An invitation joins the existing organization and its workspaces. Do not use self-service API
signup for this case: signup creates a separate workspace.

## Configure an agent or developer machine

Requirements: Python 3.12 or newer and an API key scoped to the intended workspace.

Install the lightweight client:

```bash
python -m pip install formal-engines \
  --extra-index-url https://formalengines.com/pypi/simple/
```

Install authoring support when publishing an executable environment:

```bash
python -m pip install 'formal-engines[authoring]' \
  --extra-index-url https://formalengines.com/pypi/simple/
```

Put credentials in environment variables, never in source or prompts:

```bash
export FORMAL_ENGINES_BASE_URL=https://formalengines.com/api
export FORMAL_ENGINES_API_KEY='fe_live_replace_with_workspace_key'
```

The dashboard owner or admin creates finite-lived keys under **API keys**. The plaintext key is
shown once; Formal Engines stores only its SHA-256 hash. Prefer a separate key per person, agent,
or CI system so it can be revoked independently.

## Make a read-only smoke check first

```python
from formal_engines import FormalEngines

with FormalEngines() as fe:
    runs = list(fe.training.list(limit=5))
    for run in runs:
        print(run.id, run.status, run.model.name)
```

If this fails with `401` or `403`, stop and check the base URL, workspace key, expiry, and role.
Do not compensate by pasting a secret into code.

## Work from specification to evidence

Follow this order:

1. Scaffold or obtain a verifiers-compatible environment package.
2. Validate it locally before uploading:

   ```bash
   fe spec validate ./environment
   ```

3. Publish the environment as an immutable specification version:

   ```python
   spec = fe.specifications.publish(
       path="./environment",
       train_split="train",
       eval_split="sealed_eval",
   )
   ```

4. Evaluate the base model on the sealed split.
5. Ask the human for explicit approval of the model, provider, maximum GPU count, step limit,
   time limit, and spending ceiling before starting a real training run. Formal Engines resolves
   the model revision and selects the smallest supported 2, 4, or 8 GPU layout automatically.
6. Start training with a bounded plan. Let the SDK provide idempotency and retries.
7. Stream or poll the run until a terminal state; inspect logs and metrics instead of assuming
   that `completed` means a useful model exists.
8. Require at least one registered checkpoint before claiming weights were updated:

   ```python
   run = fe.training.get("run_...").wait()
   checkpoint = run.best_checkpoint
   print(checkpoint.id, checkpoint.step, checkpoint.status, checkpoint.size_bytes)
   ```

9. Evaluate that checkpoint on the sealed split, compare it with the baseline, apply explicit
   gates, and export the signed evidence bundle.

## Run the agent improvement loop

Import newline-delimited OpenAI-compatible traces, register a reusable release gate, and let the
durable workflow connect baseline evaluation, SFT, GRPO, export, sealed candidate evaluation,
the release decision, and evidence:

```python
import time

from formal_engines import FormalEngines
from formal_engines.types import (
    CreateAgentImprovementWorkflowRequest,
    Gate,
    GrpoConfig,
    SftConfig,
    WorkflowBudget,
)

fe = FormalEngines()
dataset = fe.trace_datasets.import_jsonl(
    "support-agent-v1",
    open("support-agent.jsonl", "rb").read(),
)
while dataset.status in {"queued", "importing"}:
    time.sleep(2)
    dataset = fe.trace_datasets.get(dataset.id)
if dataset.status != "ready":
    raise RuntimeError(dataset.failure or "trace import failed")

gate = fe.releases.create_gate(
    Gate.metric("task_success", minimum=0.82),
    name="Support task success",
)
workflow = fe.workflows.create(
    CreateAgentImprovementWorkflowRequest(
        name="Support agent train and prove",
        dataset_id=dataset.id,
        specification_version_id="specv_replace_me",
        base_model_name="Qwen/Qwen2.5-0.5B-Instruct",
        sft_algorithm=SftConfig().model_dump(),
        grpo_algorithm=GrpoConfig().model_dump(),
        release_gate_ids=(gate.id,),
        budget=WorkflowBudget(max_gpu_hours=1, timeout_minutes=90),
    )
)
while workflow.status in {"queued", "running"}:
    time.sleep(5)
    workflow = fe.workflows.get(workflow.id)
if workflow.status != "completed":
    raise RuntimeError(workflow.failure or "candidate did not pass its release gate")

fe.checkpoint_exports.download(workflow.export_id, "trained-model.tar.gz")
```

Each JSONL row must contain a `messages` array with OpenAI-style `role` and `content` fields.
Tool definitions, tool calls, feedback, and a boolean success label may also be included. The
importer validates the schema, removes duplicates, detects train/evaluation leakage, rejects or
redacts sensitive values according to policy, and freezes content-addressed train, validation,
and sealed-evaluation splits. Inspect `dataset.issues`, `dataset.stats`, and `dataset.preview`
before authorizing GPU work.

The download call uses a short-lived, workspace-bound signed URL. A `ready` export includes its
format, base-model revision, digest, byte size, reload backend, inference-output digest, and the
GPU runner attestation. Prefer the PEFT adapter unless a merged model is specifically required.

## Interpret weights and checkpoints correctly

- A completed training run with no registered checkpoint did not produce a promotable output.
- A registered LoRA or distributed checkpoint contains updated parameters, but it is not
  automatically a merged Hugging Face model.
- Do not call a checkpoint better until a candidate evaluation beats the baseline under the
  declared gates.
- Do not call a checkpoint deployed until it has been converted if necessary, exported, loaded
  by an inference service, and smoke-tested.
- Preserve the base model name and revision, specification version, checkpoint digest, engine
  image digest, and evaluation run IDs in any handoff.

## Safety and cost rules for agents

- Read and list operations are safe defaults.
- Never launch, cancel, rerun, rotate a key, revoke a key, invite a member, or alter a release
  decision without explicit human authorization for that action.
- Before spending GPU time, state the exact model, maximum steps, automatic GPU ceiling,
  wall-clock limit, provider, and cost ceiling. Report the selected type/count after dispatch.
- Keep task data, environment packages, traces, checkpoints, and evidence inside the assigned
  workspace. Never move artifacts between organizations.
- Treat invitation links, API keys, Hugging Face tokens, provider keys, signed download URLs,
  and browser sessions as secrets.
- Never expose the server-held API key in client-side code. Browser access must go through the
  dashboard's same-origin session proxy.

## Troubleshooting

- `401` / `403`: wrong, expired, revoked, or wrong-workspace key; or insufficient dashboard role.
- `409` on signup: that email already owns a self-service workspace. Use a team invitation or
  have an admin create and rotate a workspace key.
- No checkpoint: inspect the terminal run state and runner logs; do not promote anything.
- Checkpoint exists but cannot be loaded: confirm its format and base-model compatibility; a
  distributed Prime RL checkpoint may need an explicit conversion/export step.
- A retry appears to create duplicates: reuse the same SDK operation or explicit idempotency key;
  do not issue a fresh raw POST.
- Capacity is unavailable: report the model, automatically selected topology, and active ceiling.
  Do not raise a cost or GPU ceiling or switch provider without fresh human approval.

When handing work back, report the organization/workspace, specification version, run IDs,
checkpoint ID and digest, evaluation comparison, release decision, and any action still requiring
a human. Never include plaintext credentials.