The AI never flies the spacecraft—and that is the point
A language model helped design spacecraft controllers, but it never gets a seat in the cockpit. The final product is a conventional control law paired with a mathematical certificate: a checkable argument that the controller meets a stated property under a stated model. In experiments on docking, spacecraft pursuit and attitude control, this arrangement let researchers use AI to search for designs without asking anyone to trust AI at flight time (Jain et al., 2026).
That separation is the paper’s central promise—and its most important limit. The models’ best results sometimes beat standard search methods, but often came close to a classical optimizer designed specifically for the task. On one nonlinear attitude-control problem, no model detectably beat a standard evolutionary optimizer when models supplied only some proposals. And a ranking among pursuit designs changed when the researchers changed how they approximated the spacecraft’s motion. The work is less a victory lap for AI than a demonstration of where its help might fit: in the design workshop, behind a gate that does not depend on the model being right.
The practical stakes are broad. Spacecraft, aircraft, medical devices and industrial robots all need controllers that act reliably when mistakes are costly. A learned system can be capable yet difficult to audit. Proof-carrying evolution asks whether a model can help explore a design space while a separate checker decides what is safe enough to keep. The answer, in these carefully bounded experiments, is a qualified yes.
The Science
A spacecraft controller is a rule for turning measurements—position, velocity or orientation, for example—into actions such as thrust. Engineers do not only want a controller that behaves well in a simulation. They may need a guarantee: that a vehicle reaches a docking tolerance within a bound, stays within a speed limit, or remains stable across a specified range of starting states.
To make such a guarantee, designers pair the control law with a certificate. In this paper, the certificate is a mathematical function whose behavior can establish properties of the controlled system. One common idea is that the function decreases as the spacecraft moves: if it shrinks at each step, the system is being driven toward a target or stable region. A certificate’s conclusion is only as broad as its assumptions. It can establish a property of the stated mathematical model, not prove that the model perfectly captures every force, sensor error or hardware fault in flight.
Proof-carrying evolution, or PCE, makes the controller and its certificate a joint search target. The researchers fixed the mathematical forms in advance. On the linear problems, the controller is a state-feedback rule and the certificate is a quadratic function; the search chooses their numerical parameters. On the attitude problem, the search chooses fifteen positive gains for a geometric proportional–derivative controller and its certificate. The language model does not write controller code or invent a proof from scratch. It proposes parameter sets. A checker tests them, and the search preferentially retains candidates whose certificates pass. Only a certified candidate can be returned as the run’s result.
The design-time / flight-time distinction matters. Once selected, the deployed artifact is the control law and its certificate. The language model is not called to choose the next thrust command. The approach therefore does not put a conversational system in a real-time control loop; instead, it uses one as a proposal mechanism in an offline engineering search. Figure 1 sketches this division of labor: a proposer suggests, a verifier checks, and selection keeps designs that satisfy the required conditions.
The researchers compared four language models with classical optimization and synthesis methods across three tasks. Docking and pursuit use a linear model of relative spacecraft motion; attitude control concerns rotations on the three-dimensional rotation group, written SO(3). Each method received paired random seeds and the same allowance of proposals: 534 per run for docking and pursuit, and 120 for attitude control. In the principal comparisons, models wrote about one in eight proposals on the linear problems and about one in five on SO(3); classical mutation filled the rest.
The verification machinery was deliberately stronger on some tasks than others. For the linear problems, certificate checks during search used exact rational arithmetic: the numbers are handled as fractions, rather than accepted based on approximate floating-point calculations. For SO(3), the search used floating-point checks, then re-checked every reported champion exactly. The best run of every method also received a proof checked by Lean 4, a formal proof system. This is a useful distinction: the search can be heuristic, but acceptance and the final proof need not rely on trusting the proposer.
What They Found
On the linear tasks, the strongest models beat the paper’s standard classical baselines on every run. That sounds decisive until the comparison is made fairer. A classical optimizer that was given the same objective and could choose certificates closed most of the gap. On docking, the paper reports no detected difference between this objective-aware optimizer and the leading models. On pursuit, the classical method beat one model and trailed another slightly. The result suggests that some apparent advantage comes not from language-model reasoning alone, but from comparing against weaker or less task-aware optimization procedures.
Docking provides a particularly revealing test of whether certification should guide search as it happens. In a controlled experiment, the researchers kept both the objective and mutation operator fixed and changed whether certified candidates were retained during evolution. With that rule, the search produced new certified designs in every run. Without it, the unverified search produced none. A later effort to find certificates for those unverified controllers recovered only 2 out of 9,399. In other words, it was not enough to search for a good controller and hope that a useful proof could be attached afterwards. In this setup, keeping certificate-feasible designs alive changed what the search could discover.
Docking objective medians across altered scenarios
Median certified docking bound, N, for methods with reported values. Lower is better. Scenario labels reflect the paper’s table; these are separate test conditions, not a single pooled experiment.
| Label | Value |
|---|---|
| Gaussian mutation — unequal thrusters | 370.5 |
| CMA-ES — unequal thrusters | 675.5 |
| Alternating SDP — unequal thrusters | 51 |
| gpt-oss — unequal thrusters | 192 |
| gpt-oss, no feedback — unequal thrusters | 283.5 |
| Gaussian mutation — tighter speed limit | 430 |
| CMA-ES — tighter speed limit | 1,005.5 |
| Alternating SDP — tighter speed limit | 64 |
The chart compares reported median docking objectives across three altered scenarios. Lower is better: the objective is a certified bound, not an observed flight time. In the unequal-thruster scenario, for example, alternating semidefinite-program synthesis reports a median of 51.0, compared with 192.0 for the model’s standard configuration and 675.5 for CMA-ES. The models are not uniformly best, and the table’s success counts matter too: the synthesis method returned qualifying results in 8 of 10 runs in that scenario, while Gaussian mutation and gpt-oss did so in 10 of 10. These are results within the paper’s particular testbed, not a general ranking of controller-design methods.
Pursuit asks whether a spacecraft can capture a maneuvering target despite the target applying bounded thrust. The strongest cited designs come with a Lean-checked theorem that covers every admissible target-thrust sequence—and thus every target strategy within the stated thrust limit. But a provocative-looking performance ranking did not survive a change in the motion model. The cited champions were ranked under Euler discretization, a simple way of approximating continuous motion in time steps. Under zero-order-hold dynamics, which treats control as held constant over each step, their ordering changed. A guarantee is meaningful only relative to its dynamics assumptions; even a small modeling choice can affect which design looks best.
The paper also probes whether model feedback improves proposals. For the pursuit task, one model’s median certified radius was 0.02960 with feedback and 0.03259 without it; smaller radii are better. The paired comparison was statistically significant after the stated correction, though the study does not establish that feedback helps generally across models and tasks. Another model’s results did not show a statistically detectable advantage. This is a reminder that “the model” is not one uniform capability: model, task, prompt, search procedure and feedback all interact.
Pursuit: feedback and the median certified capture radius
Paired pursuit results for the two model configurations reported in the feedback table. Smaller certified capture radius is better.
| Label | Value |
|---|---|
| gpt-oss with feedback | 0.04019 state-norm units |
| gpt-oss without feedback | 0.03996 state-norm units |
| Sol with feedback | 0.0296 state-norm units |
| Sol without feedback | 0.03259 state-norm units |
Attitude control on SO(3) is the nonlinear case. Here, no model detectably outperformed CMA-ES when it contributed about one proposal in five and classical mutation supplied the rest. When models wrote every proposal, one tested model improved on CMA-ES while another performed worse than its mixed variant. Even so, all search medians remained below the hand-tuned law on the attitude task. That gap points to room for better search, but the abstract does not give enough numerical results to quantify it here.
The proofs add a different kind of result. For each best run, the researchers generated a theorem corresponding to the candidate’s stated control property and checked it in Lean’s kernel. The pursuit theorem covers all permitted evader thrust sequences; the attitude designs have regional decrease certificates; and docking results include stability and speed-limit claims. The paper also reports theorems for selected docking and pursuit designs under bounded measurement noise and rounding error, conditional on an assumed bound for floating-point error. These statements are more informative than “the simulation looked stable,” but remain conditional on the model, property and assumptions that engineers chose.
Why This Changes Things
The paper’s contribution is not that a language model has learned to pilot a spacecraft. It is that a language model can participate in a search where it is not the authority on correctness. This resembles a useful pattern in computer security: an untrusted producer can suggest an artifact, while a trusted checker decides whether to accept it. Here, the model may be creative or mistaken; a failed certificate blocks its candidate from becoming the reported design.
That changes the question engineers can ask about AI. Rather than “Can we trust this model to act safely?”, one can ask “Can this model help us find a better candidate inside a design space that we know how to check?” The answer will depend on whether the chosen controller and certificate families are expressive enough. A fixed family makes formal verification tractable, but it can exclude controllers that might perform better. PCE searches parameters within the forms supplied by researchers; it does not yet discover entirely new controller structures or invent new certificate conditions.
The classical comparison is equally important. On the linear problems, models beat standard baselines, but a classical optimizer equipped to optimize the certificate for the same objective caught up substantially. This is exactly the kind of control experiment needed in AI research: compare the new ingredient not only with a convenient baseline, but with a method that has the same information and objective. If optimization can do the job more cheaply, predictably or transparently, the model may not be needed. If it finds useful candidates where classical search struggles, it may earn a role as one tool in a broader design process.
And the role should remain bounded. These experiments use abstracted dynamics and fixed parameterized controller families, not operational spacecraft or hardware-in-the-loop flight trials. Exact arithmetic can make a certificate check trustworthy relative to its equations; it cannot guarantee those equations include every real-world complication. Lean verifies that a theorem follows from its formal premises. It does not decide whether the theorem captures the mission’s true needs, or whether the chosen assumptions are realistic. Formal assurance moves uncertainty into explicit statements that can be reviewed; it does not make uncertainty disappear.
Still, the demonstrated workflow has a practical attraction. A search can try many candidate designs, including candidates proposed by a model, while the retained result carries a machine-checked argument for a stated behavior. That could make AI assistance more acceptable in domains where engineers and regulators need traceable evidence. It also creates a productive division of labor: models may help explore, optimization methods can provide structured alternatives, and proof checkers enforce a boundary neither is allowed to cross.
What’s Next
The next step is not simply to use a larger model. The paper’s own results say the comparison depends on the optimizer and on the modeling choices. Future tests need matched budgets, broader model settings, full reporting of performance and compute costs, and repeated trials across more varied dynamics. They should also examine whether the gains persist when controller families become richer, uncertainty is treated as part of the search objective, or candidate designs face higher-fidelity simulations and hardware tests.
The proof pipeline also has a clear boundary. In this work, certificate forms and proof templates are supplied in advance, so successful candidates can be translated into Lean proofs through deterministic procedures. A model-based repair step is reserved for obligations outside those templates, not used as the basis for the main reported guarantees. Extending the method to new safety properties—such as explicitly optimizing tolerance to measurement uncertainty—or to new classes of systems will require new mathematics and independently audited checks, not just a prompt asking a model to “prove it.”
The most consequential finding may be the simplest: in the controlled docking experiment, certified designs emerged when certification shaped the search, and none emerged when it was removed. It suggests that assurance need not be a final inspection bolted onto engineering after the fact. It can be part of the design objective from the beginning. If future work can scale that principle to realistic models and operational constraints, AI could help engineers search more broadly without being asked to make the final safety judgment. The spacecraft would still fly a controller—not a language model—and that separation may be what makes the assistance useful.