OpenAI Announced Its Next Model With Proofs That Compile or Fail. Steal the Gate, Not the Model.

What did OpenAI actually ship with Astra?

On August 1, 2026, OpenAI previewed its next model family, Astra, by publishing a roughly 249-page math manuscript and formal proofs in Lean 4 on GitHub instead of a press release. An internal version reportedly solved ten problems open for at least a decade, for about $2,000 of compute. Fields Medalist Timothy Gowers said he would recommend one proof for a top journal.

The detail worth copying is not the model, which is unreleased and stuck behind a planned U.S. government pre-release review. It is the proof format. A Lean 4 proof ships as a file that Lean's trusted kernel either compiles or rejects. There is no committee, no reviewer opinion, no "looks right to me." You re-run the check and get a binary answer. That is the strongest form of an acceptance gate: the output validates itself, and no amount of confident prose from the model can talk the kernel into passing a wrong proof.

Why is an LLM grading agent output the weak link?

An LLM judge is stochastic and persuadable. When you ask a model "is this Apex correct?", you get an opinion sampled from a distribution, and a self-correcting agent loop can drift or get talked into a passing verdict by its own explanation. A deterministic check cannot be persuaded. The test either passes or it does not.

This is the failure I keep seeing in agent pipelines. The Executor writes code, a Reviewer model reads the diff and says "looks good," and the pipeline advances. Two problems. First, the judge never ran the code, so it is grading plausibility, not behavior. Second, because the judge is another sampled generation, the same diff can pass on Monday and fail on Tuesday. Lean's kernel gives the same answer every time. A Salesforce deploy validation gives the same answer every time. An LLM reviewer does not, and you are building your merge decision on a coin that remembers how you phrased the question.

What is a deterministic acceptance gate in Salesforce terms?

A deterministic acceptance gate is a check that returns pass or fail from a fixed rule, not a model's judgment. In Salesforce you already own several: Apex test results with a coverage floor, sf project deploy validate against the target org, validation rules firing on DML, and JSON-schema validation on an agent's structured output. Each one compiles-or-fails the same way Lean does.

The mental move is to stop asking a model whether the work is good and start asking the platform whether the work is valid. These are the gates that already exist and cost you nothing to wire in:

• Apex tests plus a coverage floor: sf apex run test --code-coverage --result-format json. Gate on zero failures and, say, 90% coverage on the touched classes. Binary.
• Deploy validation: sf project deploy validate runs the full deployment against the real org without committing it. It fails on a broken reference, a missing field, or a failing required test. No model reads it.
• Validation rules and required fields: the DML the agent generates either survives the org's rules or throws. That throw is a gate.
• Schema and contract checks: force the agent's output through a JSON schema before anything downstream touches it. A missing field is a hard fail, not a "probably fine."

How do you wire a compile-or-fail gate into an Apex-writing agent?

Put the deterministic check inside the self-correction loop, not after it. The agent writes Apex, the pipeline runs sf apex run test and sf project deploy validate, and the raw pass/fail plus error text is fed straight back to the agent as the correction signal. The model never grades itself. The org does, and the org's answer is the loop's exit condition.

The control flow is plain:

Agent writes Apex
  -> sf project deploy validate (target: scratch/sandbox)
  -> sf apex run test --code-coverage --result-format json
  -> parse: failures == 0 AND coverage >= 90 ?
       yes -> gate passes, advance
       no  -> feed the exact failure text back to the agent, retry (cap at 2-3 rounds)

Two things make this work. The check runs against a real scratch org or sandbox, so it is grading behavior, not plausibility. And the failure text is deterministic, so the agent corrects against a concrete target ("line 42, System.NullPointerException") instead of a vague "the reviewer thinks this could be cleaner." Cap the retries so a genuinely confused agent hands you the blockers instead of burning tokens. In my own orchestrator, work items whose loop exit was a passing test suite reached the human gate far more often in one pass than the ones gated on a model's review.

When does an LLM judge still earn its place?

An LLM judge is the right tool exactly where no formal check exists. "Is this release-note wording clear?", "does this Agentforce reply match our tone?", "is this summary faithful to the record?" have no compiler. There is no kernel that compiles tone. For those, a model's judgment is the best gate you have, and pretending otherwise just means shipping with no gate at all.

So the rule is not "never use an LLM to judge." It is: if a deterministic check exists for this property, use it, and reserve the model's judgment for the properties that genuinely have no formal test. Most agent pipelines get this backwards. They use an LLM to judge correctness, which is testable, and skip judging tone, which is not. Flip it. Let the compiler own correctness and let the model own the fuzzy, human-readable properties it is actually good at.

The pattern to steal

OpenAI made its own claims checkable by anyone before it made any marketing claim at all. You can do the same for an agent that touches a Salesforce org. For every property the agent's output must satisfy, ask whether a fixed rule can decide it. If yes, that rule is the gate, and it goes inside the correction loop. If no, and only then, a model gives its opinion.

This is also where the consulting reality bites: on a large legacy org, the deterministic gates are the ones that keep an autonomous agent from touching production without a real test suite behind it. The gate is not a nice-to-have you add later. It is the thing that lets you turn the loop on at all.