The short version: a long agent run is only worth as much as your ability to trust its output without redoing the work. The way to earn that trust is not a smarter model — it's making the answer checkable. Have your agent return two things: the answer, and a certificate a cheap, deterministic program can verify on its own. The checker, not the model, decides whether the answer ships. This is exactly what OpenAI's Astra did on August 1, 2026 when it handed over Lean 4 proof certificates with its math results (The Decoder) — and the pattern scales all the way down to the agent you already run. Here's how to build it.
Step 0 — Pick a goal that can be verified#
Before any code, reframe the task so success is mechanical. An agent pointed at "write a good summary" has no certificate; an agent pointed at "summarize this document such that every claim cites a passage that contains it" does. The reframing is the whole game:
- Code → must pass a test suite and a type checker.
- Structured extraction → must satisfy a JSON Schema and a set of invariants (totals sum, dates in range, enums valid).
- Numbers / analytics → must reconcile against an independently-known total.
- Research / claims → every assertion must map to a source you can fetch and that actually contains it.
- Refactors / migrations → old and new must produce identical output on the same inputs.
If you cannot name a deterministic check, you do not have a task for an unattended agent. You have a longer thing to review — and that's a decision to make on purpose, not by accident.
Step 1 — Return a certificate next to the answer#
Make the contract explicit in the agent's output shape: the answer and the material a checker needs. For a structured-extraction task, that's the payload plus the schema it claims to satisfy:
from pydantic import BaseModel
from typing import Literal
class Invoice(BaseModel):
vendor: str
currency: Literal["USD", "EUR", "GBP"]
line_items: list[tuple[str, float]]
total: float
def check(answer: Invoice) -> tuple[bool, str]:
# Deterministic. No model. Cheaper than the extraction that produced it.
summed = round(sum(price for _, price in answer.line_items), 2)
if summed != round(answer.total, 2):
return False, f"line items sum to {summed}, but total is {answer.total}"
if answer.total <= 0:
return False, "total must be positive"
return True, "ok"
The schema (Pydantic here; a raw JSON Schema works the same) rejects malformed shapes for free. The check function encodes the invariants a valid answer must hold — the part a schema alone can't express. Note what it is not: it's not another LLM. It can't be argued with, and it can't fail in the same direction the generator did.
Step 2 — The five checkers you can build today#
You don't need a proof assistant. Five deterministic checkers cover most real work:
- Schema / type validation — the output parses and matches its contract. This is the floor, and structured-output modes from the providers get you most of the way.
- Property assertions — invariants that must hold: sums balance, dates fall in range, IDs are unique, statuses are from the allowed set. Property-based testing tools are built for exactly this.
- A re-runnable test suite — for anything code-shaped, generated code ships with tests and the certificate is
pytestexiting 0. - Reconciliation — the parts add up to a total you know independently (a control figure, a prior period, a source-of-truth API).
- Citation verification — every claim carries a source URL and a quoted span; a checker fetches the URL and confirms the span is present. No source, or a source that doesn't contain the claim → reject.
Each is deterministic, runs in seconds, and costs a fraction of the generation. That asymmetry — cheap to check, expensive to produce — is what makes verification worth doing.
Step 3 — Gate on the checker, then repair#
The certificate is only useful if it decides. Wrap generation in a bounded verify-and-repair loop: the model gets to fix its own failures, but the deterministic check is the gate.
def solve(task, generate, check, max_tries=3):
feedback = ""
for attempt in range(max_tries):
answer = generate(task, feedback) # the LLM does the work
ok, reason = check(answer) # the machine decides
if ok:
return answer, {"verified": True, "attempts": attempt + 1}
feedback = f"Your previous answer failed verification: {reason}. Fix it."
# Fail loudly. Never return unverified output as if it passed.
raise VerificationError(f"no verified answer in {max_tries} tries: {reason}")
Two rules make this safe. First: never return unverified output silently. If the loop exhausts its budget, it raises — it escalates to a human or a fallback, it does not hand back a plausible-looking guess. Second: bound it. A repair loop with no cap is a way to spend your whole token budget on one stubborn task; cap the attempts and the spend. (If you already meter agents, see how to enforce a token budget on an ai agent.)
The one thing not to do: trust a judge as the gate#
The tempting shortcut is to ask another LLM "is this correct?" and call that verification. Don't — not as the gate. An LLM judge is a probabilistic model with correlated failure modes: it can be wrong in the same direction as the generator, and a confident-sounding wrong answer is exactly the kind of thing it rubber-stamps. Use a judge as a soft triage signal if you like, but the thing that decides whether an unattended run's output ships must be deterministic — a validator, a test runner, a reconciliation, a proof. If the check can change its mind on the same input, it is an opinion, not a certificate.
Why this is the highest-leverage thing you'll build this quarter#
Astra is a research system you can't call, previewed to regulators — nothing on your roadmap should move because of a demo. But the pattern it made vivid is free, and it's the difference between an agent that saves you time and one that quietly manufactures work: a long run plus a verifier that gates it is autonomy; a long run without one is just a longer review. For the full read on what Astra signals about where the frontier is heading, see the real signal is the proof, not the problems. Then go do the small version this week — pick one unattended task, ask what machine-checkable signal proves it worked, and if the answer is "a human skims it," write that check first.



