Proof-Carrying Evolution: Black-Box Search, White-Box Flight

Introduction

Spacecraft controllers need guarantees whose assumptions and scope can be reviewed. For many critical maneuvers, opportunities for recovery are limited, so a review board asks not only whether a design worked in simulation but why it must work. Mission requirements are therefore often requirements on the strength of a guarantee under a stated model: the time within which a docking maneuver is guaranteed to reach its tolerance, the largest measurement or initial-state uncertainty under which it still succeeds, or the size of the set of states from which a vehicle is guaranteed to capture, or to evade, another under stated assumptions about its actions. Meeting such a requirement means finding both a control law and a certificate that establishes the property over the relevant operating conditions. This paper optimizes three such objectives: a certified docking-time bound, a certified capture radius against a maneuvering target, and the size of a certified attitude region on SO(3).

Classical methods such as LQR, $H_\infty$ design, gain scheduling and Lyapunov-based nonlinear design produce explicit laws that engineers can inspect and analyze, although explicit mathematical form alone does not make a complex system easy to understand. Choosing an explicit controller family still leaves a design problem: an initial law may admit no certificate in the chosen family, or its certified bound may be too weak for the mission. The certificate itself is part of this problem. Changing its parameters can improve the bound for a fixed control law, while changing the law can improve performance but lose the certificate. Searching over both gives the optimizer a way to improve what can be guaranteed.

Reinforcement learning and neural policies [39, 44] offer flexible ways to optimize constrained objectives, but their behavior can be harder to inspect and verify. A language model can instead act at design time, proposing parameters for an explicit controller and its certificate; executing the deployed law requires no model inference. We ask whether a language model can serve as the proposer inside such a certifiable design space, rather than replace it with a black box.

We call this approach proof-carrying evolution, after proof-carrying code [1]. In proof-carrying code, an untrusted producer supplies a program and a proof that it obeys a safety policy; a consumer checks the proof before accepting the program. PCE applies this separation to control design (Figure 1). A proposer modifies controller and certificate parameters, a verifier checks the certificate conditions, and selection favors candidates with better certified objective values. Retained designs provide starting points for further proposals. Only a certified candidate can become a run’s result, so acceptance depends on checking rather than on trust in the proposer. Machine checking establishes a stated property of a stated model; the choice of property and the model assumptions still require engineering review.

The experiments here use fixed controller and certificate forms: linear state feedback with a quadratic certificate on the linear problems, and a geometric proportional–derivative (PD) law with a degree-4 certificate on SO(3). The proposer chooses numerical parameters; it does not write or modify controller code. Optimizing uncertainty tolerance or a certified evasion region would extend this scope and would require new certificate conditions within this framework; here measurement noise is assessed after search (§ 7.2). The questions are whether a language model proposes better parameters than classical search and synthesis, and whether checking certificates during search helps produce certified designs. On the linear problems, the comparison depends on how the classical methods choose their certificates (§ 6.4).

Contributions.

1. Method (§ 3). PCE, an evolutionary loop in which each candidate is a controller paired with its certificate. Inside the loop the search proposes and a checker decides: certificates are checked in exact rational arithmetic on the linear problems. A certificate compiler turns a checked certificate into a Lean proof. An independent audit rejects proofs that rely on unfinished obligations or unapproved axioms.

2. Comparative evidence (§ 6.1). Four models (gpt-6-astra, gpt-5.6-sol, Claude Opus 5.5 and the open-weight gpt-oss-120b; Astra, Sol, Opus and gpt-oss below) share paired seeds and proposal allowances with classical baselines (Table tab:cross). On the linear problems, Astra and Sol beat the standard classical baselines on every run. A classical, objective-aware certificate optimizer specified before its runs shows no detected difference from either on docking; on pursuit it beats Sol and trails Astra slightly (§ 6.4). Among the cited pursuit champions, this ranking does not survive zero-order-hold dynamics (§ 7.3). These comparisons use one reasoning-effort setting per model; apart from a detected but unsized benefit for Sol on pursuit, they do not establish whether feedback improves model proposals. On SO(3), no model detectably beats CMA-ES when it writes about one proposal in five; Opus does when writing every proposal (§ 6.5).

3. Verification during search (§ 6.2.4). In a controlled docking experiment with the objective and mutation operator held fixed, retaining certified candidates produces new certified designs in every run; removing that rule produces none. Seeking new certificates afterwards recovers 2 of the 9,399 controllers produced by the unverified search.

4. Guarantees beyond simulation (§§§ 4.2, § 4.3, § 7.1 and § 7.2). The pursuit designs with Lean proofs carry a capture theorem over every admissible thrust sequence of the target, and therefore every evader strategy. Under a thrust limit, a hand-designed law and the best docking run of every arm but one have decrease theorems for the clipped dynamics. The best attitude controller of every arm has a regional decrease certificate on SO(3). The cited docking and pursuit designs also have decrease and trajectory theorems under bounded measurement noise and rounding error, assuming a bound on floating-point error.

5. Exploratory optimizer studies (§ 6.6). The search itself need not be trusted, since the checker decides what we keep. On docking, we gave a language model control of the whole search, testing four optimizers with one model and, for one optimizer, four model configurations. Each combination used two seeds and the same exact evaluator. Every newer configuration lowered the cost on both seeds. The ordering of the optimizers changed with the seed, though, and their time and price differed by one to two orders of magnitude. Every final champion carries an audited Lean certificate. One optimizer also read an archived answer when its sandbox allowed it, so we need to isolate the proposer as part of the method.

Related work

Language models in evolutionary search and in proof.

FunSearch [2], AlphaEvolve [3] and ShinkaEvolve [4] use a language model as the mutation operator of an evolutionary search over programs, and showed that such loops can discover new algorithms under automated evaluation; ShinkaEvolve targets the number of evaluations the search needs. Fitness in those systems is empirical; it does not establish formal properties of the surviving code. PCE uses the same propose, evaluate and select loop, with certificate checks governing acceptance. Our search space consists of numerical parameters for fixed controller and certificate forms. Searching over controller structure, as those systems search over program code, remains outside our experiments.

Goedel-Prover V2 [5] uses an open 32B model with Lean compiler feedback. It reports 90.4% on MiniF2F (pass@32, with self-correction). DeepSeek-Prover-V2 [46] and AlphaProof [47] also prove competition mathematics. To our knowledge, none gates engineering synthesis. In PCE a prover would repair obligations beyond the templates (§ 7.4); all obligations here have templates (§ 3.2).

Verina [6] tests joint generation of code, specification and proof in Lean. Its best frontier model proves 4.9% of tasks in one trial without compiler feedback. Our obligations are more structured: once a certificate passes its exact check, a deterministic template can construct the proof. We therefore use templates for the reported designs and test model-based proof repair separately (§ 7.4).

Language models as optimizers.

Language models are used for more than evolutionary program search. They can act as general-purpose optimizers, proposing candidates from earlier results and evaluation feedback [62]. The problems range from prompts and heuristics to model pipelines, as in DSPy and GEPA [58, 49]. More recent approaches let agents write, execute and refine code, and even change their own workflows [53, 59, 56]. How much of the search the model controls differs between these methods, but they all use external evaluation to guide the next improvements. We use a similar approach in PCE, with a separate decision about acceptance: the model can explore freely, while a deterministic certificate checker decides which candidates can be accepted.

Model or procedure.

How much of an improvement comes from the model, and how much from the optimization procedure? Studies find that both can matter substantially, but a more elaborate search does not necessarily beat a simpler one [64, 52]. Agent benchmarks show a similar dependence on the model, the agent scaffold and their interaction [51, 55]. Sometimes a simple pipeline matches a more elaborate agent, and no optimization strategy does best on every problem [61, 60]. We therefore need to account for the computational cost and what the search procedure contributes, as well as the final performance [54]. We use random search and genetic algorithms as model-free baselines for this reason. PCE also lets us examine two settings: campaigns with the model inside a fixed search loop, and optimizer experiments in which it runs the whole search (§ 6.6).

Certified control and certificate synthesis.

[7] provide a systematic stability library in Lean 4 and mathlib, following machine-checked control and ODE theory in Coq and Isabelle [8, 9, 10]. These are libraries; they perform no synthesis. Closer to PCE, [12] formally certify sum-of-squares Lyapunov functions for polynomial systems in Minlog, Pegasus [13] generates continuous invariants that KeYmaera X then proves, and VeriPhy [14] carries a verified hybrid-system model through to a verified controller executable. Each certifies or compiles a given controller or model, but none searches for the controller. Our generated obligations follow the same spirit: docking certificates lift per-step checks to trajectories by an induction the generator emits, and pursuit certificates by one shared handwritten lemma, seq_affine_decay. On the synthesis side, FOSSIL 2.0 and the CEGIS line [11] synthesize Lyapunov and barrier certificates, and controllers with them, as neural templates checked by satisfiability-modulo-theories (SMT) solvers; trust rests on the solver and its floating-point interface. PCE replaces the solver in the trust base with a proof kernel, through exact rational sum-of-squares (SOS) witnesses.

Learning and assurance in spacecraft control.

Earlier work by the present authors and colleagues placed language models in the control loop itself. Prompted and fine-tuned agents flew spacecraft in Kerbal Space Program differential games, from text and from screenshots [36, 37, 45]. Small fine-tuned models emitted control vectors for orbit transfer, cislunar control and powered descent [38], and a model trained by group relative policy optimization reasoned its way to control actions [42]. That line followed learned policies for landing and multi-phase ascent [39, 44] and compact recursive networks for optimal control [43]; language has also conditioned safe rendezvous trajectory generation [40]. In each case the learned model acts at flight time or the safety of its output rests on the optimizer that produced it. Closest in spirit is AutoResearch [41], in which a language model drives the research loop offline, never operates the vehicle, and has each result certified against the problem’s measured seed noise, a statistical credibility layer. PCE likewise keeps the model at design time but makes the credibility layer formal. Where learned policies do fly, run-time assurance wraps reinforcement-learning policies for docking and inspection in control-barrier-function shields [15, 16, 17], and neural Lyapunov–barrier methods verify trained controllers after the fact [18]. Those approaches retain a learned policy in the deployed controller; PCE uses the model only during design. Separating untrusted search from trusted checking is not new; to our knowledge, the new combination is a model jointly proposing controller and certificate parameters in an evolutionary loop, admission by exact certificate check, and kernel-checked theorems for reported designs.

Method

The loop

PCE searches over a fixed family of controllers and certificates. A candidate is one choice of their parameters $\theta$, specifying a control law $u = \pi_\theta(x)$ and a function $V_\theta$. The certificate conditions express the desired closed-loop property, such as decrease of $V_\theta$ within a region. On the linear problems the controller is linear state feedback $u = Kz$ and the certificate a quadratic Lyapunov function $V(z) = z^\top P z$, so a candidate is the pair $(K, P)$; it is stored as $(K, L)$ with $P = LL^\top$, which makes $P$ positive definite by construction. On SO(3) a candidate is fifteen positive diagonal gains that set both the controller and the certificate (§ 4.3). Following evolutionary-search usage, we call the stored parameter vector the candidate’s genome. A generation consists of proposal, checking and selection. The retained candidates form the elite, and the best certified candidate of a run is its champion. Table 1 lists what is searched and checked on each problem.

At each generation (Figure 1), a language model or classical operator proposes candidates, typically by modifying retained designs. Each is checked and scored using the problem’s rules (Table 1). On the linear problems, a tiered verifier checks certification and a simulator measures mission cost. On SO(3), a floating-point certificate program determines both admissibility and score.

Selection retains a fixed-size elite. In the main campaigns, the objective is a certified value, so certified candidates rank ahead of uncertified ones. Uncertified candidates survive only when too few certified candidates are available to fill the elite. In the control experiment ranked by simulated cost (§ 6.2.4), half the elite places are reserved for certified candidates. A run returns its best certified candidate. § 4 defines the problems, and Appendix § 10 gives the search settings.

Problem	Parameters searched	Check during the search	Check afterwards
Docking	gain $K$ and certificate factor $L$	exact: stability, the speed-limit envelope and the docking bound $N$	Lean proof for the best run of each arm
Pursuit	gain $K$ and certificate factor $L$	exact: robust decrease and the capture radius	exact re-certification of each champion; Lean proof for the best run of each arm
SO(3)	fifteen diagonal gains of the controller and the certificate	floating point: regional decrease, by a linear program	exact re-check of each champion and of the positivity of $V$; Lean proof for the best run of each arm and for the hand-tuned law

Checking certificates instead of searching for proofs

On the linear problems, the verifier checks each certificate condition (§ 4.1) by testing positive definiteness of a quadratic form. This is sufficient for the required nonnegativity and provides an exact witness: a weighted sum-of-squares decomposition [21, 22], computed by $LDL^\top$ factorization in exact rational arithmetic. A non-positive pivot fails this check and rejects the candidate. The check takes milliseconds without calling Lean. A successful factorization supplies the proof data: the generated Lean file states the decomposition as a polynomial identity with the exact coefficients as data, so checking it needs no proof search, no language model and no external solver (Appendix § 11).

Verification proceeds in tiers. Tier 0 rejects candidates using numerical spectral-radius checks and, on docking, rollout divergence. Tier 1 is the exact rational check, which performs the same mathematics that Lean verifies, but at evolutionary throughput. Tier 2, repair by a language model with compiler feedback, is held in reserve for obligations that no template covers (§ 7.4). On the two linear problems every certification decision in this paper was made at tier 1, by construction. On SO(3) the loop admits candidates with a floating-point program, and every counted champion is re-verified at tier 1 afterwards (§ 6.5).

Which designs receive Lean proofs.

Lean independently checks proofs for the best run of every arm in Tables tab:docking, Table 5 and tab:so3, including the optimizer and model-only controls, and the tightest pursuit-sweep designs. SO(3) proofs retain each run’s gains, region level and contraction target.

Other proved designs are the champions of Astra’s three docking control experiments, gpt-oss’s best static-prompt pursuit run, the preliminary single-run designs discussed in § 6, the hand-designed saturated law, and the proof-repair file. The hand-tuned SO(3) law and exact manifold-preserving step also have proofs. We call these designs cited.

For each, the Lean 4 kernel [24] checks the proof and an independent audit permits only Lean’s three standard axioms (Appendix § 11). The kernel cannot check intent; theorem statements and model assumptions require review (§ 8).

These rules make verifiability part of selection: the search must find a controller that performs well and admits a certificate in the chosen family.

Proposers

Every third generation the model proposes eight candidates; Gaussian mutation supplies the rest (Table 2). Prompts show the elite’s genomes, scores, certification status and objective, and state the certification requirements. Replies are parsed and, on the linear problems, clamped to fixed gain bounds. Failed calls are replaced by Gaussian children.

We use bare requests with no system prompt or declared tools for all four models. They cannot execute anything in the panel (but the CLI controls of § 6.2.2 and the optimizers of § 5.0.0.5 can execute code). Astra and Sol share a gateway; Opus uses its provider’s API; gpt-oss runs locally from pinned weights. We log all prompts, replies and token counts. The models all use low reasoning effort. Sampling uses each provider’s defaults; we did not set or equalize sampling across providers. The closed models returned the aliases we requested (gpt-6-astra, gpt-5.6-sol, claude-opus-5-5) rather than dated snapshots; we identify them by name and call dates, 13–27 September 2026. We use a pinned revision of gpt-oss.

The non-LLM operator is Gaussian mutation with Lyapunov repair. Half its children perturb both controller and certificate parameters. The other half mutate $K$ and re-solve the discrete Lyapunov equation for the modified loop. This baseline therefore also uses control-specific structure. On SO(3), where there is no corresponding Lyapunov equation to solve, mutation multiplies each gain by a log-normal factor. Model proposals take seconds to minutes, whereas exact checks take milliseconds, so the loop checks every child and queries the model only every third generation.

Search cost is metered in proposals: every distinct genome offered for evaluation is charged to a ledger shared by all arms, so an equal budget means an equal number of proposals offered, not an equal number of generations.

In the optimizer studies (§ 5.0.0.5), we go a step further and give the language model more control over the search, rather than just proposing candidates within a fixed evolutionary loop. The evaluator, budget counter and audit trail remain independent of the model, so all candidates are still checked under the same conditions. We compare different approaches, from predefined optimization strategies to agents that can organize and adapt their own search process.

Three use engines from GEPA’s optimize_anything framework, which we refer to as GOA [50]. GOA GEPA uses reflective evolution, where the model revises candidates based on previous results and evaluator feedback [49]. GOA Meta-Harness gives a coding agent access to the history of previous candidates, their scores and feedback, allowing it to run code and propose up to ten new candidates per iteration [59]. GOA Omni combines several optimization strategies [60]. In our configuration, GEPA, Meta-Harness and AutoResearch each receive 62 evaluations, followed by 187 evaluations for GEPA and another 187 for Meta-Harness, with each stage initialized from the best candidate found so far.

We also study a more autonomous approach using prime-agent, a self-evolving agent harness built around a persistent Python environment and recursive subagents [57]. Rather than acting as an optimizer with a predefined search strategy, it follows an AutoResearch-like process in which the agent writes and executes code to explore candidate solutions, while reflecting on previous results and adapting its own search procedure during execution. This allows us to test whether giving the model control not only over the candidates, but also over how the search is conducted, leads to better results.

Despite these differences, all approaches submit genomes as text to the same exact checker, with every evaluation counted against the same proposal budget. We also include random search and the Gaussian-only evolutionary loop of § 3.1 as model-free baselines. Appendix Table 9 provides the configurations, limits and feedback used in each approach.

The three problems

The method is applied to three problems on two dynamics models: docking and pursuit on the linear Clohessy–Wiltshire plant, and attitude control on SO(3).

Docking

Our first testbed is in-plane rendezvous under the Clohessy–Wiltshire equations [19], with mean motion $n = 1.13\times 10^{-3}$ rad/s and an Euler discretization at $\Delta t = 1$ s. The state $z = (x, y, v_x, v_y)$ holds positions in metres and velocities in metres per second. The mission initial conditions lie at $\left\lVert r_0 \right\rVert \approx 1.1$–$1.3$ m from the target, so the task is the final part of an approach. The equations can be expressed in other length units if all corresponding constants are rescaled. Here, the speed limit allows 0.2 m/s at the target, the saturated actuator considered below delivers at most 0.2 m/s$^2$, and the pursuit evader of § 4.2 thrusts up to 0.01 m/s$^2$. The docking tolerance and pursuit capture radius use the unweighted state norm, combining the numerical position and velocity components in the stated units. Thus a radius $r$ bounds both miss distance and residual speed ($r = 0.02$ means 2 cm and 2 cm/s). This weighting is a comparison convention, not a mission requirement.

The thrust is $u = Kz$, unbounded in the model except in the saturated case at the end of this subsection. Safety is expressed as the distance-dependent speed limit $\left\lVert v \right\rVert \le \nu_0 + \nu_1 \left\lVert r \right\rVert$ ($\nu_0 = 0.2$, $\nu_1 = 0.5$), which we inner-approximate by the polynomial safe set $h(z) = \nu_0^2 + \nu_1^2 (x^2 + y^2) - v_x^2 - v_y^2 \ge 0$. The certificate is the quadratic function $V(z) = z^\top P z$ with $P = LL^\top$ (§ 3.1). Writing $H_0=\operatorname{diag}(\nu_1^2,\nu_1^2,-1,-1)$ gives $h(z)=\nu_0^2+z^\top H_0z$. Let $\mathcal Z_0$ be the mission initial set listed in Appendix § 10, and define $c_{\mathrm{needed}}=\max_{z_0\in\mathcal Z_0}V(z_0)$, the smallest Lyapunov level containing those starts. Coverage requires $c_{\mathrm{needed}}\le c$.

For each candidate, fast numerics estimate the decrease margin, the S-procedure multiplier and the envelope level $c$. These estimates are rounded conservatively and then checked exactly. For the cited designs (§ 3.2), the certificate compiler generates Lean proofs of the following properties:

• Stability: $\alpha\left\lVert z \right\rVert^2 \le V(z) \le \beta\left\lVert z \right\rVert^2$ and $V(z^+) \le \rho\, V(z)$, hence $V(z_n) \le \rho^n V(z_0)$. The contraction $\rho$ is certified directly (Appendix § 13 compares this with a padded proxy): a bisection whose test is exact, bracketed by a floating-point generalized eigenvalue, finds the tightest contraction, which is rounded up to a rational, and the exact check confirms $\rho P - A_{\mathrm{cl}}^\top P A_{\mathrm{cl}} \succ 0$ at that value. Here $\alpha$ and $\beta$ bound the size of $V$, and $\rho<1$ bounds its contraction per step.

• Safety: the envelope $\Omega_c = \{V \le c\}$ lies inside $\{h \ge 0\}$ by the S-procedure [20]. For a multiplier $\lambda\ge0$, the checks $H_0+\lambda P\succeq0$ and $\lambda c\le\nu_0^2$ imply $h(z)\ge\nu_0^2-\lambda V(z)\ge\nu_0^2-\lambda c\ge0$ on $\Omega_c$. The envelope is forward-invariant, so every trajectory that starts in $\Omega_c$ satisfies the speed limit at every future step (safe_forever).

• Coverage and docking time: each mission initial condition satisfies $V(z_0)\le c_{\mathrm{needed}}\le c$. From each such start, the state is within the docking tolerance after $N$ steps and stays there (docking_within_N, docking_stays_within). For a cited design the headline number is thus itself a kernel-checked theorem.

For each mission start, the stability inequalities give $\alpha\left\lVert z_n \right\rVert^2\le V(z_n)\le\rho^nV(z_0)\le\rho^n c_{\mathrm{needed}}$. The objective is therefore the certified docking-time bound $N = \min\{\, n : \rho^{\,n}\, c_{\mathrm{needed}} \le \alpha r^2 \,\}$ for the state-norm tolerance $r = 0.02$. It is computed and re-verified in exact arithmetic; § 7.5 explains why this is not optional. Selection therefore acts on what can be proved rather than on what is observed.

Saturating actuators.

The docking model above leaves the thrust unbounded. When the thrust saturates, $u = \mathrm{sat}(Kz)$ componentwise on $[-u_m, u_m]$, the closed loop becomes piecewise and no single polynomial identity covers it. Writing the deadzone as $\psi = Kz - \mathrm{sat}(Kz)$, the loop becomes $z^+ = A_{\mathrm{cl}} z - B\psi$, and $\psi$ satisfies a regional sector condition [26]: for diagonal $T \succeq 0$ and $G = \theta K$, if $|((K - G)z)_i| \le u_m$ then $\psi^\top T(\psi - Gz) \le 0$. The certificate is then a joint SOS in $(z, \psi)$,

together with one row per thruster placing $\{V \le c\}$ inside the region where the sector condition holds. The generated Lean file treats each thruster as below, inside or above its unsaturated range. It states nine cell lemmas, one for each pair of thruster states, with a separate SOS identity for each cell. A dispatch theorem combines the cases. This proof needs case analysis as well as polynomial identities, but a template still generates it. § 7.4 tests whether a language model can reconstruct parts of this proof.

Pursuit of a maneuvering target

The second problem, on the same plant, adds adversarial robustness. A maneuvering target with bounded thrust enters the relative dynamics as a disturbance, $z^+ = A_{\mathrm{cl}} z + Bw$ with $\left\lVert w \right\rVert^2 \le w_{\max}^2$. A joint S-procedure certifies the robust decrease $V(z^+) \le \rho_r V(z) + \delta$ for every admissible $w$ through

which is checked exactly at tier 1. A handwritten lemma (seq_affine_decay), proved in Lean like every other statement, lifts this per-step bound to trajectories under arbitrary bounded disturbance sequences. A corollary, pursuit_bound_feedback, quantifies over every state-feedback evader strategy with admissible thrust (Listing lst:leansample). A simulator can only sample opponent strategies, whereas the kernel-checked theorem covers all of them. The objective is the certified ultimate capture radius $r_{\mathrm{cap}} = \sqrt{C_{\mathrm{cap}}/\alpha}$ with $C_{\mathrm{cap}} = \delta/(1 - \rho_r)$, the radius that this bound approaches as $n \to \infty$; in finite time, the corollary certifies entry into $1.5\,r_{\mathrm{cap}}$ from a stated step $N$ onward. No actuator limit is modeled for the pursuer.

theorem pursuit_bound_feedback (g : $\mathbb{R}^4 \to \mathbb{R} \times \mathbb{R}$)
    (hg : $\forall$ q, (g q).1$^2$ + (g q).2$^2$ $\le$ $w_{\max}^2$)
    (p : $\mathbb{R}^4$) (n : $\mathbb{N}$) :
    V (trajS g p n) $\le$ $\rho_r^{\,n}$ * V p + $\delta$ / (1 - $\rho_r$) := $\ldots$

Attitude control on SO(3)

Docking and pursuit share the same Clohessy–Wiltshire dynamics; they are two problems on one linear model, differing in the certificate structure (quadratic envelope versus robust S-procedure) and the objective. On both, every certificate condition is a linear matrix inequality in the certificate’s parameters. Rigid-body attitude is different. The state is a rotation matrix together with a body rate, the decrease condition is a degree-4 polynomial inequality in twelve variables on SO(3), and the guarantee is necessarily regional, because no continuous feedback stabilizes SO(3) globally [33]. We step the dynamics with the Cayley transform at $h = 0.1$ s, which maps a rational rotation to an exactly rational rotation, so every certificate concerns a state that lies exactly on the manifold. With inertia $J$, diagonal gains $\widehat G, G_c, M, C, K_\omega$, $\Psi(R) = \operatorname{tr}(\widehat G(I - R))$ and $e_R = (G_c R - R^\top G_c)^\vee$, the controller and certificate are

and the theorem states $V(x^+) \le \rho\, V(x)$ on the region $\{V \le c\}$. The certificate is a sum-of-squares identity with multipliers for the manifold constraints and an S-procedure term for the region. We find it with a linear program over Gram matrices that are diagonally dominant under a fixed diagonal scaling, re-estimated between solves [23], then rationalize it and re-derive it over $\mathbb{Q}$.

Positive definiteness of $V$ requires a separate exact check: a sum-of-squares lower bound $V \ge \alpha\left\lVert y \right\rVert^2$ in centered coordinates. The search screen requires positive gains, but the cross term involving $C$ means that positive gains alone do not ensure positive definiteness. We therefore check this property for every counted champion after search (§ 6.5). Because the gains are diagonal, the problem has a Klein four-group symmetry that splits the 90-monomial basis of the decrease certificate into blocks of sizes $27 \oplus 21 \oplus 21 \oplus 21$.

We report the size of the region as the largest attitude error, about any axis, that it is guaranteed to contain at rest, $\theta_{\max} = \arccos\bigl(1 - c/(\operatorname{tr}\widehat G - \min_i \hat g_i)\bigr)$; a state with nonzero rate must satisfy the full condition $V \le c$. The score is this certified angle rather than the level of $V$, which a rescaled gain would inflate at no cost. In the geometric PD family [35, 34], the certificate is tied to the controller ($\widehat G=G_c$, $M=J$). A hand-tuned law has a certified region containing every attitude at rest with error up to 126.9$^\circ$, with $\rho=0.9937$. The kernel checks the manifold-preserving step in SO3Step and regional decrease with a non-empty-region witness in SO3AttitudePD.

Figure 2 shows the certificate’s cost and conservatism. As the region approaches the antipodal set, its contraction approaches one; beyond it no certificate is found. From rest near the region’s edge, the simulated trajectory decays much faster than the envelope, with the first ten steps computed exactly. Commanded torque remains well below its certified bound.

Experimental setup

Problems and objectives.

On docking (§ 4.1) the objective is to minimize the certified docking-time bound $N$; on pursuit (§ 4.2) it is to minimize the certified capture radius $r_{\mathrm{cap}}$; and on attitude control (§ 4.3) it is to maximize the attitude error that the certified region contains at rest. Each problem uses one certificate formulation throughout. An arm is one proposer or baseline with fixed settings. Arms share the campaign’s seeds and proposal-accounting rules (Table 2). Population-based arms receive the same initial population on each seed; the pursuit PD grid instead uses its own lattice. SO(3) populations are deliberately drawn from a weak part of the controller family.

	Docking	Pursuit	SO(3) attitude
Objective	bound $N$ (min.)	radius $r_{\mathrm{cap}}$ (min.)	angle $\theta_{\max}$ (max.)
Paired seeds	20	20	20
Population $\times$ generations	$28 \times 24$	$28\times 24$	$12 \times 10$
Proposal allowance per run	534	534	120
Model proposals	a batch of eight every third generation
Share written by the model	about 1 in 8	about 1 in 8	about 1 in 5
Other	–	evader thrust $\le 0.01$ m/s$^2$	$\rho \le 0.995$, weak start

Proposers and baselines.

The four models of § 3.3 run on all three problems. They are compared with Gaussian mutation with Lyapunov repair, with CMA-ES [27] over the same genome, and with a structured classical method for each linear problem. On docking this method is classical synthesis by an alternating pair of semidefinite programs over $(K, P)$ on a grid of target contraction rates [20, 28]. It is a local BMI search rather than a certificate of optimality, and we run it both to the end of its own grid and, with seeded restarts, to the full allowance (“own grid” and “full allowance” in the tables). On pursuit the structured method is a PD grid matched to the allowance, with each gain paired with a certificate from the textbook Lyapunov repair. We call these the standard classical baselines. A further classical optimizer chooses certificates for each objective, as described below. We report a panel of four models; other evaluated models are outside the reported panel. Astra and Opus also run through their providers’ coding-agent command-line tools (“CLI”) in the interface controls (§ 6.2.2).

Classical certificate optimization.

The standard baselines choose their certificates by textbook rules: the pursuit grid closes each gain with a Lyapunov-equation repair at three shape weights, and docking synthesis maximizes an absolute contraction margin under a trace cap, which is not the docking bound. The language models propose gain and certificate together, so their advantage could come from better certificate choices. To test this explanation we added, after the main campaigns, a classical optimizer that shapes the certificate for each problem’s objective, from classical starting gains only. Its comparison family (against Astra and Sol on both problems, Holm over four) and the reading of each outcome were fixed in code before its runs.

Both objectives are invariant to certificate scale, which each subproblem fixes. At a fixed gain and rate, the certificate SDP minimizes $\mu$ on pursuit subject to $P\succeq I$ and $M_{\mathrm{rob}}\succeq0$, minimizing $r_{\mathrm{cap}}^2=\mu w_{\max}^2/((1-\rho_r)\alpha)$. On docking it maximizes $\alpha$ subject to $P\succeq\alpha I$, mission-start levels at most one, contraction and the safety envelope; this minimizes $N$ at that rate. With the certificate fixed, a second SDP improves the gain because the Schur conditions are affine in $K$.

Pursuit also admits jointly convex invariant-ellipsoid synthesis at each rate in $Q=P^{-1}$ and $Y=KQ$ [20]; docking’s envelope does not. Each run evaluates the shared initial population and applies the certificate step to every gain in that population and in a PD lattice. Pursuit also runs joint synthesis on 33 rates. Gain and certificate steps then alternate from the best candidates until the proposal allowance or 20,000-call solver cap is reached. All candidates use the same exact evaluator and ledger.

Control experiments.

Each control changes one setting, except the joint effort/ceiling experiments (Table 3). Interface controls use Astra’s CLI with and without execution, and Opus’s CLI. Reasoning controls use gpt-oss and Claude Fable 5.1 (Fable), a model used only in these controls, at low and high effort. High effort also raises the output ceiling: from 16,000 to 32,000 for Fable, and from 16,000 to 28,000 for gpt-oss. Further gpt-oss arms vary these settings separately, using a three-comparison family fixed before calls.

Static-prompt controls show Astra, gpt-oss and, on pursuit, Sol only the initial elite. Gate controls remove verification from Gaussian search or retain it with the objective fixed (§ 6.2.4).

Optimizer studies.

The docking studies vary the optimizer and model along two axes (Figure 3). On the optimizer axis, we compare GOA GEPA, GOA Meta-Harness, GOA Omni and prime-agent (§ 3.3) with gpt-5.6-sol (Sol 5.6) at medium effort. On the model axis, we fix prime-agent and compare Sol 5.6 with Astra, gpt-6-sol and Opus at xhigh effort. prime-agent was among the best-performing approaches in the first phase. Its flexible harness lets each model adapt its own search strategy. We chose it for the model comparison for these reasons. The axes share prime-agent with Sol 5.6 as a baseline, giving seven combinations rather than sixteen. We cannot separate model and reasoning-effort effects on the second axis, since both change together.

We run each combination on two seeds (0 and 1), with two docking objectives, giving 28 runs. One objective is the simulated cost $J$ (Appendix § 10); the other is the padded proxy $N_{\mathrm{proxy}}$ (Appendix § 13), whose final designs we rescore on the actual bound $N$ (§ 4.1). The same seed gives each approach the same initial design. A run can submit at most 560 genomes to the checker, and every submission counts, valid or not. We compare cost at a shared checkpoint of 491 evaluations.

Random search and the Gaussian-only GA provide references without a model. Random search evaluates the shared starting design followed by 559 independent samples, selecting directly on $J$ or $N$. The GA instead starts with its own random population; it uses 560 evaluations for cost and 672 for the bound. Every approach uses the same exact checker, and only certified candidates can become champions. We re-certify and audit the final designs. The optimizers run in isolated sandboxes with no access to the evaluator (§ 7.5).

Given the two seeds per combination, we treat the comparisons as descriptive, reporting both seeds and considering a difference consistent only when it has the same sign in both. We report tokens, time and price separately, since equal evaluation budgets do not imply equal computational costs. Comparisons with the campaigns are limited by different budget accounting, unpaired seeds and the use of the proxy for bound optimization. Full run configurations and results are provided in Appendix Table tab:optruns and the corresponding results tables.

Statistical analysis.

The unit of analysis is a run, and comparisons pair arms by seed. Population-based arms share their initial population within each pair. All twenty runs in a base campaign solve the same problem instance: $n$ counts repeated searches, not independent control problems. When a deterministic baseline is compared with an arm that returns the same design on every run, as for Astra against the pursuit PD grid, the comparison measures repeatability on that instance. We report medians because docking bounds are integers with frequent ties, and a few weak runs produce long tails in both linear objectives.

For each comparison we report the median paired difference, a percentile bootstrap 95% confidence interval (20,000 resamples of paired differences; pointwise, without multiplicity adjustment), and W / L / T (wins, losses, ties) seed counts. The two-sided Wilcoxon signed-rank test [31] drops zero differences. It uses the exact distribution without tied ranks, exact permutations for tied ranks among at most thirteen differences, and otherwise the normal approximation without continuity correction. At $n=20$ without ties, its smallest attainable $p$ is $1.9\times 10^{-6}$.

The test concerns symmetry of paired differences about zero. We interpret small $p$ as evidence that an arm has a consistent within-seed advantage, not as a test of the median; the interval describes the median effect.

Campaign tests use Holm adjustment [32] over stated families (Appendix § 13). Docking and pursuit families were fixed after results and are exploratory. SO(3), control and optimizer families were fixed in code before their runs. Other tests are exploratory and unadjusted; model orderings are descriptive. No equivalence margin was set, so an undetected difference does not establish that no difference exists.

A run that loses more than a quarter of its model calls is excluded as degenerate; the rule excludes five runs, and Appendix § 13 gives its history and a sensitivity check under which no median difference changes sign.

Results

Overview across the three problems

Table tab:cross compares the four models across the problems. Each model is paired by seed with the strongest standard classical baseline: full-allowance alternating-SDP synthesis on docking, the PD grid on pursuit, and CMA-ES on SO(3). The linear problems also include the certificate optimizer. Comparisons use twenty paired seeds, or nineteen when a run is excluded as degenerate. The table gives medians and win/loss/tie counts; Tables tab:docking, Table 5 and tab:so3 give paired differences and Holm-adjusted $p$-values.

Astra and Sol beat the strongest standard baseline on every run of both linear problems. gpt-oss loses to that baseline on every run; Opus loses on most docking runs but wins on most pursuit runs. Certificate optimization closes most of Astra and Sol’s advantage (§ 6.4). The ordering changes on SO(3): Astra matches CMA-ES in median, Sol ranks last, and Opus and gpt-oss lie between them. The hand-tuned SO(3) law has a larger certified angle than any search arm’s median. In the optimizer studies reported in the last subsection (§ 6.6), a language model runs the whole search.

Docking

The campaign

Table tab:docking and Figure 4 report the docking campaign. The paired design compares arms that start from the same population on each seed. In Table tab:docking, “Spent” is the median number of proposals offered before an arm stops or exhausts its allowance. “Tokens” is the median output tokens per model call, including reasoning. The reference is synthesis at the full allowance. Above the last horizontal rule, $p$-values are Holm-adjusted over the 7 campaign comparisons.

The final rows report classical methods added after the main campaign: CMA-ES with BIPOP restarts and a smaller initial step (Appendix Table tab:baselines), and the certificate optimizer (§ 5.0.0.3). Their comparisons with synthesis are outside the campaign family; raw $p$-values are shown in parentheses. The optimizer stops at its solver-call cap.

Synthesis is the strongest standard classical baseline by a wide margin (Table tab:docking). Astra and Sol beat it at the full allowance on every seed, with median bounds of 38.5 and 38 steps. Opus and gpt-oss rarely or never beat synthesis. Astra and Sol also spend the most reasoning (Table tab:docking). Objective-aware certificate optimization closes most of their lead over the standard classical baselines. No difference between the certificate optimizer and either leading model is detected in the declared comparison family (§ 6.4).

Figure 5 shows how the searches progress. The medians of the two leading models fall to near their final bounds with the first model batch and change little afterwards; Opus and gpt-oss improve in steps over the whole run, and Gaussian mutation stays near the seeded population’s bound until the last generations.

CMA-ES stops early because its initial step, set by the shared pool’s spread, is too wide for the certifiable set: nearly every child is uncertified and the fitness landscape is flat (Figure 4b). Same-step restarts [29] do not help. BIPOP restarts [30] with the step scaled by $0.01$ spend the allowance and improve the median to 121 steps (Table tab:docking). The rerun beats Gaussian mutation on 18 of 20 seeds, but loses to synthesis and both leading models on every seed. It also trails Opus and gpt-oss on 18 of 20 and 14 of 20 seeds. The step scaling was the best tried and is therefore tuned (Appendix Table tab:baselines).

Structure of the champions.

Astra approximately cancels the Coriolis coupling in 20 of 20 runs, but the measured benefit is at most about one step (Appendix Table tab:coriolis). The Lyapunov factor proposed with the gain tracks the bound (Appendix § 13).

Figure 6 shows a typical Astra certificate, from seed 1 at the arm’s most common bound, kernel-checked with 19 theorems. Its envelope $\sqrt{\rho^k c_{\mathrm{needed}}/\alpha}$ bounds the simulated trajectories, which enter the tolerance before $N$. These sampled trajectories enter early, but they do not determine the worst-case entry time over all certified starts. The exact projection of the certified set contains the three mission starts and their trajectories and lies inside the polynomial safety boundary $\|v\|^2=\nu_0^2+\nu_1^2\|r\|^2$.

Thrust.

The comparison uses unbounded actuators and establishes no ranking under a thrust limit. Model champions have gentle simulated peaks, while synthesis commands more; on every run its certified envelope admits states that would command more than 0.2 m/s$^2$ (Supplementary Table 10). No campaign imposes the limit on all arms. The best run of each arm is checked under it afterwards (§ 7.1).

(a)

(b)

Control experiments on the proposer

Each experiment compares settings of the same model, paired by seed (Table 3). Most change one setting; the joint reasoning-effort controls also change the output ceiling. Experiments concern docking unless stated otherwise. The Opus interface family covers all three problems; its row in the table reports docking.

The table gives medians over paired seeds and unadjusted two-sided Wilcoxon $p$-values, followed in parentheses by Holm-adjusted values where a comparison family was declared. The docking static-prompt controls use the base problem and seeds of the modified-instance campaign (§ 6.2.3).

Interface.

Astra’s execution-enabled CLI let the model run Python outside the proposal ledger; the other CLI variant disabled execution. Session accounting and the Opus CLI setup are given in Appendix § 13. Neither CLI variant differs detectably from the API arm at twenty runs (Table 3).

For Opus, no interface difference is detected on any problem in the family fixed before the API calls (Holm $p \ge 0.94$). Pursuit wins split 10 to 10, and SO(3) wins 10 to 10. The API-minus-CLI intervals are $[-4.5,7.0]$ steps on docking, $[-6.2\times 10^{-4},2.9\times 10^{-4}]$ in radius on pursuit, and $[-2.9,2.9]^\circ$ on SO(3).

Reasoning budget.

The shared effort setting bought different amounts of reasoning (Table tab:docking); Fable used a median of 1,089 output tokens per call. Raising effort and the output ceiling helped Fable, which used 15,838 tokens per call and finished within a step of the leading models (Table 3). For gpt-oss, using 7,487 tokens per call, no difference was detected in the comparison fixed before its calls. The low-minus-high interval, $[-25,+18]$ steps, still permits an effect that matters.

Changing effort and ceiling separately also detected no difference (Table 3). At low effort no call approached either ceiling (median 1,123 output tokens), so the differing search medians reflect run-to-run variation. At high effort, 7 of 160 calls reached the lower ceiling; the interval for the ceiling comparison was $[-29.5, 2]$ steps.

These controls do not isolate the role of reasoning in the cross-model ordering: changing the effort setting also changes how the model generates proposals. The observed token use is therefore needed to interpret the configuration comparisons. Astra and Sol were not rerun at other efforts.

Feedback.

Astra’s static-prompt control sees only the initial elite, so every call samples the same prompt. Its first batch certifies a median bound of 41.0 steps, against 40.0 with feedback; selection among later draws closes the gap. On the base problem, no feedback benefit is detected for Astra on the 12 paired seeds (Table 3). The static-prompt result limits what we can attribute to feedback. The separate verification experiment (§ 6.2.4) tests the benefit of retaining certified designs during selection. gpt-oss is ahead with feedback on most docking runs and behind on most pursuit runs, with neither difference detected (Table 3). Its first batch’s certified bound is far above its final docking bound.

				median
5-6 Control	A	B	$n$	A	B	A / B / T	$p$ (Holm $p$)
interface	Astra (coding agent)	Astra	20	38	38.5	11 / 6 / 3	$0.18$
interface	Astra (text-only)	Astra	20	38.5	38.5	6 / 5 / 9	$0.72$
interface	Opus (CLI)	Opus	20	66.5	68.5	11 / 8 / 1	$0.31$ ($0.94$)
reasoning effort	Fable (effort low)	Fable (effort high)	20	49.5	39	2 / 17 / 1	$2.5\times 10^{-4}$
reasoning effort	gpt-oss	gpt-oss (effort high)	20	95	95.5	10 / 9 / 1	$0.70$
feedback	Astra	Astra (no feedback)	12	38.0	38.0	2 / 5 / 5	$0.41$ ($0.59$)
feedback	gpt-oss	gpt-oss (no feedback)	20	95.0	104.5	13 / 7 / 0	$0.0592$ ($0.24$)
feedback (pursuit)	gpt-oss	gpt-oss (no feedback)	19	0.04019	0.03996	7 / 12 / 0	$0.28$ ($0.55$)
feedback (pursuit)	Sol	Sol (no feedback)	20	0.02960	0.03259	12 / 6 / 2	$0.0483$ ($0.0483$)
output ceiling	gpt-oss (low, 16k)	gpt-oss (low, 28k)	20	95	97	7 / 11 / 2	$0.98$ ($0.99$)
reasoning effort	gpt-oss (low, 28k)	gpt-oss (high, 28k)	20	97	95.5	8 / 11 / 1	$0.49$ ($0.99$)
output ceiling	gpt-oss (high, 16k)	gpt-oss (high, 28k)	20	87	95.5	13 / 6 / 1	$0.31$ ($0.94$)

Transfer to modified problems

Astra’s first batch is within a few steps of its final bound on all but 1 runs. Sol’s first-batch median is 41 steps, although 8 of its 20 runs remain above 100 steps. To probe search versus recall, we fixed variants with the cross-track thruster at half strength, a tighter speed limit, an initial set a quarter farther out and geostationary mean motion. A seeded-population feasibility probe preceded instance selection; selection preceded the campaign.

Unchanged base designs transfer to geostationary orbit with at most a step’s change in any arm’s median (Appendix Table tab:transfer). Under unequal thrust, classical champions still certify on every seed, while Astra’s text-only champions certify on only 1: their nominal gains assume symmetric actuation. Under the tighter limit and wider initial set, none of the leading arms’ champions certifies, although the seeded population still has certified members.

The campaign uses 10 seeds per arm on the modified problems on which the leading base designs transfer least successfully (Table 4). Gaussian mutation and CMA-ES need two to six times their base bounds. Synthesis remains close to its base-problem bound on the seeds it certifies (Table 4). On unequal thrust, preserving certified starting designs makes synthesis certify every seed (Appendix Table tab:baselines).

When told about unequal thrust, Astra and Fable at high effort recover the base problem’s bound, although most of their unchanged base-problem champions do not certify on that plant (1 and 4 of 20, Appendix Table tab:transfer). Provider spending caps allow only partial samples and stop every run on the other modified problems before completion. The experiment is incomplete for these models; even complete, it would test adaptation to a stated change rather than distinguish recall from reasoning. gpt-oss beats Gaussian mutation and loses to synthesis on every instance.

	unequal thrusters	tighter speed limit	wider initial set
2-3(lr)4-5(lr)6-7 Arm	cert.	median $N$	cert.	median $N$	cert.	median $N$
Gaussian mutation	10/10	370.5	8/10	430.0	10/10	454.0
CMA-ES	10/10	675.5	8/10	1005.5	10/10	610.0
alternating SDP synthesis (full allowance)	8/10$^{\dagger}$	51.0	10/10	64.0	10/10	62.0
Astra	4/4	38.0	–	–	–	–
Fable (effort high)	8/8	38.0	–	–	–	–
gpt-oss	10/10	192.0	9/10	154.0	10/10	104.0
gpt-oss (no feedback)	10/10	283.5	8/10	97.5	10/10	142.5

Verification during search versus afterwards

Searching on simulated performance and certifying afterwards can fail even when simulation looks safe. LQR with $Q=R=I$ has spectral radius 0.4224 and violates no sampled speed limit, yet our completion finds no certificate. Aggressive LQR-class gains also violate no sampled constraint and certify stability, yet no safety certificate is found: no admissible level both covers the mission starts and lies inside the speed-limit set.

These failures do not establish that the controllers are unsafe. They mean that the controllers do not meet our certificate requirements. A safety certificate must cover every state in its envelope at every future sample instant; a rollout checks only the trajectories simulated.

We reran Gaussian search without verification, keeping its operator and seeded populations and ranking by simulated mission cost. Exact checking afterwards certifies no member of any final population under either certificate formulation (Table tab:filter).

Checking the whole search history finds that every certified genome came from the initial population. None of the 10,120 genomes produced by search certifies. After the first generation, no population member certifies. By comparison, search with verification retains certified candidates in every run.

The next control holds the simulated-cost objective fixed and changes only selection. With verification, half the elite places are reserved for certified candidates; without it, candidates are retained solely by simulated cost. The verification rule produces 515 certified genomes out of 10,120 new proposals, compared with 0 without the rule (Table tab:filter).

The objective still affects the quality of the certified designs. With the verification rule in place, ranking by simulated cost ends at a median bound of 344 steps; ranking by the certified bound gives 152 steps.

We also sought fresh certificates for the 9,399 controllers produced after initialization that pass the spectral screen, out of 10,120 produced in total. Lyapunov-equation repairs at eight weightings certify 0; the synthesis SDP at twenty rates certifies 2 (Table tab:filter). The recovered controllers are on seeds 18 and 19, with bounds 88 and 223 steps. The SDP search took 3.7 worker-hours.

These procedures do certify controllers from the initial population. Their limited success on later controllers suggests that replacing the certificate alone does not recover certification under the tested procedures. Other certificates may still exist. In this experiment, verification acted as a selection pressure during the search, not as a filter that could be applied afterwards.

Pursuit

The campaign

Pursuit (§ 4.2) tests the same search methods with an adversarial disturbance. The objective is the certified capture radius $r_{\mathrm{cap}}$ against an evader whose thrust is bounded by 0.01 m/s$^2$. Figure 7 shows the task for one certified controller, the PD grid’s, kernel-checked as CWHPursuitPdGridS0: the target keeps thrusting and turning, and the theorem bounds the relative state for every admissible evader, not only for the one simulated. In panel (b) the filled disk is the projection onto the position plane of the capture ball $\|z\| \le 1.5\,r_{\mathrm{cap}}$ that the kernel-checked corollary certifies from step $N$ on, and the dashed circle is $r_{\mathrm{cap}}$; panel (c) shows the envelope $\sqrt{(\rho_r^k V_0 + C_{\mathrm{cap}})/\alpha}$, with $N$ marked.

A preliminary single-run law certifies $r_{\mathrm{cap}}=0.02857$ under the campaign formulation and 0.03086 under the formulation used to find it. Its significant parameters are $k_p\approx0.75$, $k_d\approx1.75$ and two Coriolis-cancelling gains. An attack over 5,003 adversarial steps finds no violation of the certified bound; its strongest tail radius is 0.01333, which does not establish the worst-case radius. Replacing the evolved certificate with the textbook shape worsens the bound to 0.04522 at the same gains: the certificate is part of the design.

The PD grid searches log-spaced gains $k_p \in [0.02,2]$ and $k_d \in [0.1,4]$ at three Lyapunov shape weights. It is sized to the allowance, and failed repairs count against it. It is deterministic at each allowance, so paired comparisons measure the other arm’s variation.

Astra and Sol lead the panel, beating every standard classical baseline on every seed (Table 5; Figure 8). Their median radii are 0.02857 and 0.02960. The certificate optimizer closes most of this advantage: the signed-rank test detects a benefit over Sol, while Astra retains a small lead in the declared comparison family (§ 6.4). Astra returns the same design every time, so its wins against the deterministic grid measure repeatability on this instance; Sol varies across runs.

The table also reports first-batch radii. In the figure, the dashed line is a 48-point PD scan re-certified under the campaign formulation, and positive paired differences favor the arm. Campaign tests are Holm-adjusted; the optimizer’s test is raw and outside that family.

Astra proposes its final design in the first batch (Table 5). On 20 of 20 seeds it matches the preliminary single-run reference within $5\times 10^{-6}$; this is also the best design found by a finer sweep of robust synthesis (§ 6.4).

Sol reaches the same radius within that tolerance on 4 seeds, through later proposals and selection. Its first-batch radius is 0.04444 (Table 5). The static-prompt control also improves, starting at 0.0492, but finishes worse on most seeds (Table 3). The signed-rank test detects a feedback benefit in the single-pair family declared before the calls. The median paired difference, $+0.0033$, has interval $[-0.0004, 0.0046]$, which includes zero.

Opus (0.02986) is ahead of the PD grid on 16 of 20 runs and beats Gaussian mutation on every seed (Table 5; Supplementary Table tab:supppursuit). Its advantage over the grid is fragile: the CLI wins just as often, but its losses are larger (raw $p = 0.0266$ against $1.0\times 10^{-4}$ for the API arm). No difference between gpt-oss and Gaussian mutation is detected (Supplementary Table tab:supppursuit).

Every retained run certifies: 1 of 240 reported-arm runs was excluded as degenerate, and every champion re-certifies at its recorded radius. The best run of each arm, including the optimizer, and the tightest budget-sweep champions have Lean proofs: 12 certificates with 11 theorems each.

These radii compare unbounded-thrust designs. Simulated peak thrusts far exceed the 0.2 m/s$^2$ saturated-actuator limit (Supplementary Table 10).

		$r_{\mathrm{cap}}$	vs. PD grid
3-5(l)6-8 Arm	Cert.	Median	Best	First batch	med. $\Delta r$	W / L / T	Holm
Gaussian mutation	20/20	0.04140	0.03671	–	$+0.0075$	0 / 20 / 0	$4.0\times 10^{-5}$
CMA-ES	20/20	0.04446	0.03696	–	$+0.0106$	0 / 20 / 0	$4.0\times 10^{-5}$
PD grid search$^{\dagger}$	20/20	0.03388	0.03388	–	reference
Astra	20/20	0.02857	0.02857	0.02857	$-0.0053$	20 / 0 / 0	$9.3\times 10^{-5}$
Sol	20/20	0.02960	0.02857	0.04444	$-0.0043$	20 / 0 / 0	$9.0\times 10^{-4}$
Opus	20/20	0.02986	0.02870	0.04935	$-0.0040$	16 / 4 / 0	$9.4\times 10^{-4}$
gpt-oss	20/20	0.04009	0.03446	0.06100	$+0.0062$	0 / 20 / 0	$4.0\times 10^{-5}$
certificate optimizer$^{\ddagger}$	20/20	0.02862	0.02859	–	$-0.0053$	20 / 0 / 0	($8.8\times 10^{-5}$)

Effect of the search budget

We reran Gaussian mutation, CMA-ES, the PD grid and gpt-oss on seeds 0–9 at twice and four times the generations, allowing 1,062 and 2,118 proposals. CMA-ES and the grid were matched to Gaussian mutation’s spend (Table 6; Figure 9).

CMA-ES improves with budget and beats Gaussian mutation on every seed at both larger allowances; its champions converge on the preliminary single-run reference’s gains. gpt-oss and Gaussian mutation barely improve. The latter’s schedule shrinks its step to $2.2\times 10^{-6}$ in the longest run; the schedule was not varied, so the plateau is conditional on it.

The allowance-specific PD grids are not nested, which explains their nonmonotone scores. A single lattice refined with the allowance has the same score at every allowance (Appendix Table tab:baselines). It shows no detected difference from CMA-ES at twice the allowance and loses on every seed at four times.

On the ten sweep seeds at the largest allowance, CMA-ES approaches but does not reach Astra’s first-batch radius (0.02943 against 0.02857) and is already below Sol’s original-allowance median. Astra and Sol were run only at the original allowance, so the sweep does not establish how they scale.

Arm	$\times1$ (24 gen.)	$\times2$ (48 gen.)	$\times4$ (96 gen.)
Gaussian mutation	0.04039	0.03861	0.03850
CMA-ES	0.04577	0.03418	0.02943
PD grid search	0.03388	0.03879	0.03563
gpt-oss	0.03946	0.03739	0.03703

Random mutation improves the certified pursuit radius, whereas it makes little progress on docking. This pattern is consistent with a more restrictive certifiable set on docking; the experiments do not isolate feasibility geometry from the other differences between the problems. The textbook controller-only grid plateaus; every arm beating it chooses the certificate with the controller (Table 5 and Table 6; § 6.4).

The guarantee remains stronger than simulation: pursuit_bound covers every admissible thrust sequence, hence every evader strategy regardless of its information. Listing lst:leansample’s corollary states the state-feedback case.

Classical certificate optimization on the linear problems

The standard baselines use textbook certificate choices, while the models choose controller and certificate parameters together. The optimizer of § 5.0.0.3 tests how much of the models’ advantage remains when a classical method also chooses certificates for the objective. Its results are the final rows of Tables tab:docking and Table 5.

On docking the optimizer reaches a median of 40 steps, ahead of synthesis at the full allowance on all 20 seeds, with a median paired advantage of 12.5 steps. Shaping the certificate at fixed classical gains alone reaches 41. No difference from either leading model is detected (Supplementary Table tab:suppcertopt). The bootstrap intervals describe median paired differences and do not establish equivalence. Sol’s interval excludes zero although the Holm-adjusted signed-rank test does not detect a difference. The interval is pointwise and concerns the median; the test uses the signed ranks and adjusts for the declared comparison family.

On pursuit the optimizer reaches 0.02862. The signed-rank test detects a benefit over Sol, although the median-difference interval $[-3.2\times 10^{-3}, 1.6\times 10^{-5}]$ includes zero. Astra remains ahead on every seed by a median of $+5.1\times 10^{-5}$, with interval $[4.3\times 10^{-5}, 8.3\times 10^{-5}]$ (Supplementary Table tab:suppcertopt). The gap is 0.2% of Astra’s radius. The optimizer beats Opus and gpt-oss on every seed on both problems.

An exploratory finer rate sweep, run after the campaign, reaches Astra’s radius, 0.02857, at $1-\rho_r = 0.5$. This seed-independent joint program shows that refining the rate grid can close the remaining gap. It is convex only at a fixed rate: the sweep finds a best value, not a proven optimum.

Objective-aware certificates explain most of the leading models’ advantage. Astra’s pursuit lead survives the declared comparison; an exploratory finer rate sweep of textbook synthesis reaches the same radius. This compares equal proposal allowances, not equal computation: the optimizer uses medians of 238 proposals on docking and 340 on pursuit before its solver cap. Median solver time is 3 and 8 minutes per run.

The optimizer is local and provides no global optimality guarantee. Taken together, these results do not establish a model advantage over classical design on the linear problems. Astra reaches its result in the first batch; Sol improves through later proposals and selection. Classical certificate optimization reaches comparable scores.

Attitude control on SO(3)

The campaign.

SO(3) tests whether the linear-problem ranking extends to a nonlinear manifold, using the known law of § 4.3 as reference. The panel searches fifteen diagonal gains from weak seeded populations (median best 88.1$^\circ$), with Table 2’s allowance. Every proposal counts against the allowance, certified or not, and is scored by the floating-point linear program.

Exact re-verification accepts 158 of 158 counted champions with their angles unchanged. This checks decrease, not positivity of $V$. A separate exact check finds all 158 positive definite, with smallest $\alpha=0.34$. The best run of each arm also has a Lean proof of regional decrease, torque bound and a non-empty region at its own gains, level and contraction target (Supplementary Table tab:coverage).

Table tab:so3 and Figure 10 report the campaign. The table’s Gain measures improvement over the shared initial best; its tests are Holm-adjusted over the 15 pairs of the campaign arms. The rows below the line report the model-only control.

CMA-ES is the strongest classical arm, and no model in this mixed design is detectably better. Astra matches its median of 105.2$^\circ$ and beats Gaussian mutation by $+7.3^\circ$ ($p = 0.0023$). Opus lies between the baselines in median, and CMA-ES beats Sol (Table tab:so3). No arm reaches its final value in the first model batch; the medians rise in steps over the allowance (Figure 10c). The best medians remain 21.7$^\circ$ below the hand-tuned law, which no run of this mixed design reaches. The deliberately weak starts make this a test of recovery within the allowance, not of the best design in the family.

Image not extracted

Control experiment: models writing every proposal.

Opus through its CLI and Sol also wrote every proposal, replacing the mixed design’s model share of about one in five. The control has its own family of 6 comparisons (Table tab:so3).

Opus improves to 115.7$^\circ$ and beats its CLI mixed arm by $+11.0^\circ$. It wins that comparison on 19 of 20 seeds ($p = 1.7\times 10^{-5}$). It is the only arm detectably better than CMA-ES (Table tab:so3). Its median remains below the hand-tuned law, but one run reaches 128.2$^\circ$ at rest with $\rho = 0.99487$. This contracts more slowly than the hand-tuned law’s $\rho = 0.9937$, nearer the cap. The controller remains geometric PD; its certificate uses independent weights outside the tied family ($\widehat G \ne G_c$, $M \ne J$).

Sol instead falls to 93.7$^\circ$, with paired change $-6.5^\circ$ against its mixed arm ($p = 0.0017$), and trails CMA-ES on every seed (Table tab:so3). Each call requests twelve controllers. Sol supplies near-copies, while Opus varies its proposals more widely. Increasing the model’s share of proposals therefore has opposite effects for these configurations. This comparison also uses nine or ten model calls where CMA-ES uses none, so it compares the stated search configurations without matching inference cost.

Optimizer studies: models that run the whole search

The optimizer studies (§ 5.0.0.5) ask how much the final performance depends on the search strategy and how much on the model. Figure 11 shows the final certified cost $J$ and bound $N$ for the two docking objectives. There are only two seeds for each combination, so we describe the results and call an improvement consistent only if it occurs on both. The bound runs optimize the padded proxy $N_{\mathrm{proxy}}$, but the figure gives the actual bound $N$ of their final designs. Appendix Tables tab:optall and tab:optruns give the complete results for both axes.

Final performance across approaches.

Final costs for the three newer models lie between 0.73 and 0.76 on both seeds (Figure 11a). These values are 82 to 85% below the starting design and 42 to 44% below LQR with $Q = R = I$ ($J = 1.31$), although our completion procedure cannot certify the reference controller (§ 6.2.4). The range is wider when we keep Sol 5.6 fixed and change the optimizer: 0.81 to 1.99 across the four approaches. The model-free references, random search and the Gaussian-only GA, have costs between 1.88 and 3.02.

Most approaches also improve the bound substantially from the starting designs’ 231 and 477 steps (Figure 11b). Of the 14 bound runs, 11 finish between 56 and 80 steps. GOA GEPA is an exception, at 146 and 208 steps, as is the Opus run stopped by its time limit, at 2,896 steps. That Opus design has the same proxy score as Astra’s seed-1 design ($N_{\mathrm{proxy}} = 8{,}594$), yet Astra’s certified bound is 59 steps. Similar proxy scores can therefore correspond to quite different certified bounds.

The final designs differ between objectives. Optimizing the bound gives costs from 1.99 to 3.57, whereas optimizing cost gives bounds from 205 to 7,224 steps. These results suggest that an improvement on one objective need not carry over to the other, so the choice of optimization target matters.

The optimizer or the model.

The best optimizer changes with the seed when we keep Sol 5.6 fixed (Figure 12a). prime-agent has the lowest cost on seed 0 and the highest on seed 1. Relative to it, the GOA engines have 26 to 146% higher costs on the first seed, but 21 to 22% lower costs on the second (Figure 13a). With prime-agent fixed instead, all three newer models lower cost relative to Sol 5.6 on both seeds: by 6 to 10% on seed 0 and 43 to 44% on seed 1. The checkpoint affects the size of this gap. The Sol baseline on seed 1 continued from 1.33 at 491 evaluations to 1.21 at completion, but the improvement still holds on both seeds.

Although neither axis shows a larger effect on both seeds, the newer models produce much more consistent results, with final costs differing by less than 2% between seeds and 5% between models. In comparison, the Sol 5.6 optimizers show differences of up to a factor of 1.9 between seeds. For the bound objective (Figure 13b), the differences are smaller, with GOA Meta-Harness being the only optimizer to improve over the Sol baseline on both seeds, by just one and two steps, while none of the newer models improves the bound on either seed.

We also repeated prime-agent with Opus on the cost objective, running it three times on seed 0 with different stopping limits and once on seed 1 (Figure 14). The runs followed different search paths and completed between 206 and 560 evaluations, but all finished with very similar costs, between 0.757 and 0.760. In the shortest run, the operator interrupted a computation after two hours and asked the agent to keep subsequent computations short, although its best design had already been found. These runs do not establish repeatability under identical conditions, but the small variation in their final costs suggests that the different search paths can still lead to similar solutions.

The final designs also show a clear relationship between cost and position gain (Figure 15). The starting designs have gains $k_p$ between 0.010 and 0.013, while the GOA engines reach 0.024 to 0.042 and the newer models 0.068 to 0.083. In general, larger gains correspond to lower costs, although the other parameters of $K$ and the certificate also change, so this relationship cannot be attributed to position gain alone.

With Sol 5.6 fixed, the optimizers differ widely in what they spend (Appendix Figure 17 and Table tab:optall). A GOA run took 2 to 5 hours and a median of 8 to 48 million tokens, $12 to $46 at list price; a prime-agent run took 8 to 11 minutes and about one million tokens, $0.25 to $1.49. Per logged call, the prime-agent runs averaged 3 to 33 designs sent to the checker, often from scripts that submit many genomes, compared with 2 to 9 for the GOA engines. A check takes milliseconds and model inference seconds to minutes, so batching plausibly accounts for part of the gap in time; context length and latency also play a role. The newer models reached a cost below 0.8 within 3 to 22 minutes of the start; no GOA run went below 1. The optimizers log different operations as model calls (for example, a reflection, an agent session or an agent turn), so calls are not comparable units of inference.

Rejection rates change during the search (Appendix Figure 18). For prime-agent, 24 to 45% of the first hundred candidates are rejected, compared with 7 to 24% afterwards. Astra’s failures due to insufficient margins for the exact checker fall from 12.5% to 0.1%. Most remaining failures for Sol 5.6, Astra and gpt-6-sol have a safe region that does not contain the mission start. Opus still fails mainly on thin margins: 69 of its 93 rejections. GOA GEPA and GOA Omni instead show a slight rise in rejections, from 4 and 7% to 13 and 10%, mostly from a failed decrease condition or insufficient margins. Random search has much higher rejection rates, around 76 to 77%, mostly for invalid safe regions. Every optimizer receives the failing condition and numerical hints as feedback, but these observations describe the search over time. They do not establish that feedback caused the improvement.

We can also compare the final designs with the earlier campaigns, although the different objectives and budgets prevent a direct comparison. Under the campaigns’ objective, most bound-run designs certify between 56 and 80 steps, apart from the three exceptions discussed above. These bounds are higher than those obtained by synthesis at the full allowance (52), Astra, Sol and the certificate optimizer (38.5, 38 and 40), but ten of the eleven are lower than the Opus campaign result (68.5). The campaigns optimized $N$ directly over twenty seeds, while these studies used the padded proxy. In fact, the relationship between the two objectives is relatively weak, with Spearman correlations of $+0.07$ across the 14 main bound runs and $+0.37$ across all 22 docking-bound designs, including pilots and repeats (Appendix Figure 16).

These studies suggest that model choice can matter substantially when the search procedure lets the model adapt its strategy. With prime-agent fixed, all three newer models lower the cost on both seeds and reach similar final designs. Changing the optimizer with Sol 5.6 fixed is less consistent: the ranking changes with the seed, and computational costs differ by one to two orders of magnitude. We cannot fully separate model and effort effects, or measure their interaction with the optimizer, because model and reasoning effort change together and we tested only one row and one column of the full grid. All 28 final champions passed the exact checker and carry audited, kernel-checked Lean certificates. The studies cover docking only, not pursuit or SO(3).

Verification beyond the campaigns

A certified controller with saturating thrusters

For a hand-designed law at thrust limit $u_m=1/5$, the completion of § 4.1.0.1 gives $\theta=1/5$ and $\rho_s=0.986409$. Its envelope, $c=4.4128$, covers the mission starts ($c_{\mathrm{needed}}=1.03$).

The audited file has 942 lines and 29 declarations covering the cell lemmas, dispatch and trajectory chain. Because decrease holds only inside $\{V\le c\}$, the global iterate lemma does not apply. Instead, sat_trajectory proves invariance and geometric decay together: invariance supplies the region hypothesis needed for decay. This yields bounded thrust and an enter-and-remain bound of 641 steps.

The proof covers the true clipped dynamics. The theorem saturation_active_witness gives $z=(0, 0, 0, -3/4)$ with $V(z)=3.59\le c$ and commanded thrust $0.23>u_m$. The mission-start simulations never saturate in 1,200 steps. Only the theorem covers off-nominal states in the certified region where saturation is active.

At the same limit, using each design’s own gain and certificate, completion certifies 11 of 12 cited docking champions, each with an audited Lean file. The optimizer is the exception: no searched sector parameter both covers the mission starts and admits a multiplier. This is a failure to find a certificate.

The saturated settling bounds are 1.0–2.2 times the linear bounds. Exact witnesses activate saturation in 8 designs. For the others, searched states do not saturate, so their certificates do not establish that the limit is reached.

Measurement noise and rounding

A flight computer measures $z + n$ and evaluates $K(z+n)$ in floating point, so the applied thrust is $K(z+n) + e$ with $e$ the rounding error. Both errors reach the plant through $B$, as the evader’s thrust does on pursuit, and each becomes a bounded channel of the robust decrease of § 4.2, with one S-procedure multiplier per channel and every cross term kept in the exact LDL$^\top$ check. The measurement error is bounded by $\left\lVert n \right\rVert \le \bar n$ in the state’s own units, and $\left\lVert Kn \right\rVert \le \sigma \bar n$ with $\sigma^2 I - K^\top K \succ 0$ checked exactly. The rounding error follows the standard model of binary arithmetic [48]: on the certified invariant set, $|e_i| \le \gamma_5 \sum_j |K_{ij}|\,|z_j + n_j|$ plus an underflow term, with $\gamma_5 = 5u/(1-5u)$ for unit roundoff $u$.

All 24 cited docking and pursuit designs remain certified with their own gains and certificate matrices. The targets were fixed before computation: on docking the ultimate bound must remain inside the tolerance and the safety envelope invariant; on pursuit the radius must be at most $1.5\,r_{\mathrm{cap}}$.

The admissible measurement-error bound is $\bar n=0.000498$–$0.000966$ on docking, or 2.5–4.8% of its tolerance. On pursuit it is $\bar n=0.00259$–$0.00341$. Double precision changes no bound to three figures; single precision reduces none by more than 0.4%.

At half the admissible noise bound, docking takes 1.05–2.1 times the noise-free certified steps. The certificate allocates contraction to disturbance rejection, using a split chosen for the smallest ultimate bound rather than the fastest docking. On pursuit the steps to $2\,r_{\mathrm{cap}}$ increase by at most 1.

Each design’s audited Lean file states the update from $A$, $B$ and $K$, proves it equals the disturbed step, and proves decrease and trajectory bounds for every bounded noise, rounding-error and evader-thrust sequence. The floating-point bound is a hypothesis, not a theorem.

The zero-order-hold plant

Every certificate on the linear problems is for the Euler step. A thruster that holds its command over the step gives instead the zero-order-hold plant $z^+ = A_d z + B_d u$, with $A_d = e^{A_c \Delta t}$ and $B_d = \int_0^{\Delta t} e^{A_c s}\,ds\,B_c$. It is exact at the sample instants for the stated continuous-time model. Unlike the Euler step, it includes the effect of thrust on position within the interval, whose leading term is $\Delta t^2/2$ per unit acceleration. We enclose $A_d$ and $B_d$ by exact rational Taylor sums of order 22, with every neglected entry below $1.2\times 10^{-22}$, and re-check each design’s own gain and certificate matrix against every plant in the enclosure by exact LDL$^\top$, the perturbation entering through Young’s inequality. The settings and outcomes were fixed before the full computation.

All 24 cited designs retain a certificate. Docking step counts change by factors of 0.78–1.08. Of these designs, 8 need at most 3 more steps; 4 need fewer.

On pursuit, we also held the evader’s thrust over each step and separated the six tightest Euler designs (radius at most 0.0318) from the other six. The tight group includes Astra, Sol, Opus and the optimizer. Its certified radii grow by factors of 2.9–4.7; the others grow by 1.04–1.55. An Euler-shaped certificate explains some, but not all, of this growth.

An exploratory simulation, not fixed in advance, uses the search’s greedy evader and the largest distance over the last 100 of 600 steps. In the tight group this distance grows by 1.5–2.4 times, to 0.029–0.043. For the rest it changes by 0.83–1.6 times and stays below 0.024. Among the cited pursuit champions, the Euler leaders lose their lead on the zero-order-hold plant. The trajectory comparison above is exploratory; it does not establish a new paired-campaign ranking. The certificate checks use exact rational Python arithmetic, without Lean; the exploratory trajectories are simulations.

Proof repair by a language model

The campaign certificates all have proof templates. In the recorded Codex CLI repair experiment, we removed the proofs of two saturated cells, cell_DD and cell_UU, from a reduced file that retains a complete proof of cell_LL. A language model then attempted to fill the missing proofs, initially marked with sorry.

The model receives the reduced file and an author-written proof plan. Appendix § 11 gives the repair protocol and recorded model settings.

The recorded comparison uses attempts with and without a supplied identity. Without the witness, all 4 attempts on cell_DD fail. With it, both obligations close on their first attempts, taking 84 s and 94 s. The shared witness is an exact identity bounding the first thruster’s sector on the certified region; its longest integer has 46 digits.

This does not show that the model lacked the identity: 2 failed attempts already state it exactly. Attempts in both conditions also write decrease coefficients with integers up to 104 digits. The prompts and compiler messages were not retained, so the failed step is unknown.

These are successful reconstructions in the condition with a supplied identity. They do not establish why the outcomes differ, estimate a general repair success rate, or demonstrate repair beyond the template’s reach.

Without a supplied plan, gpt-oss attempts 11 obligations: the saturated certificate’s nine cells and the SO(3) decrease and torque bound. This is a separate experiment with a different model, not a controlled test of removing the first experiment’s plan. Its obligations, conditions and settings were fixed before any call; the protocol is in Appendix § 11.

The same acceptance gate admits all 11 generator proofs. gpt-oss closes 0 obligations without the witness and 0 with it, across 88 calls. An exploratory audit of the last attempts finds the complete long-integer identity in 8 of 9 witnessed cell attempts; they fail later. Without witnesses, 3 attempts invoke the dispatch theorem that depends on the cells themselves. At this effort and without a plan, the model does not assemble these proofs. A stronger prover was not tried.

Auditing the pipeline

The Lean kernel checks control theorems; exact arithmetic checks linear admissibility, step counts and SO(3) champions; floating-point statistics, simulation and forensics produce every comparison between arms and the search scores. Appendix Table 7 assigns each statement to its checking layer.

Four adversarial reviews of the lower two layers, run as separate author-orchestrated LLM-agent sessions with distinct briefs and archived attacks, confirmed the certificate mathematics and exposed two defects.

Floating-point logarithms can undercount a bound by one step: $\rho=99996/100000$ gives $N=10{,}000$ where exact arithmetic requires $10{,}001$. Exact re-verification left every shipped bound unchanged and is now required for every reported $N$.

Build-log axiom reports can be forged with #eval IO.println; the original build-log audit accepted a proof of False. An independent Lean.collectAxioms driver now checks dependencies directly. A negative regression test injects axiom fake : False and requires rejection.

We also had to consider risks from the proposer, independently of the checker. A model with file access may find earlier solutions, and coding agents have been observed trying to bypass their sandbox restrictions [63]. This happened in an initial GEPA pilot on the docking bound (§ 6.6). The coding-agent CLI used a read-only sandbox but inherited the repository as its working directory. The model found an archived champion from an earlier LLM-GA run and returned it as its own proposal. The proposal matched all 24 genome values and the proxy bound of 9,484 steps. After we hid the repository, the same seed reached 24,629 steps, a 2.6 times worse result. We excluded the contaminated run from the studies.

The model could read previous results without write access. An empty working directory did not take away read access either: it could still use absolute paths. For all the later runs we used an allowlist sandbox to hide the repository and the previous results. We also had to exclude another source of previous answers, namely the prompts and replies that the CLI saves from earlier sessions. We therefore isolated each run with a separate home directory. The evaluator is a separate external service, so the agent cannot manipulate the budget counter and audit trail. We also compared the submitted genomes and model replies with previous champions. This way we can detect an exact copy, but data can leak without an exact copy in the model reply. That is why we combine the comparison with sandbox isolation, rather than relying on the comparison alone.

Continuous integration builds and audits every generated certificate, regenerates 5 of them from the archived genomes, compares their bytes and theorem lists with a pinned manifest (97 theorems), and re-audits every certificate the paper cites. Model-written and template-written proofs face the same kernel check and axiom audit. Using a model to propose a proof therefore does not require trusting the model.

Discussion and limitations

Scope of the guarantees.

Guarantees concern rationalized controllers and certificates over exact reals at sample instants: Euler steps at $\Delta t=1$ s on the linear problems and Cayley steps at $h=0.1$ s on SO(3) (Supplementary Table tab:coverage).

Linear measurement noise and rounding are covered only as bounded errors; the floating-point error bound is assumed, not proved. SO(3) noise, sensor bias and noise with thrust saturation are uncovered. Docking champions are checked under a thrust limit only after search; their speed-limit envelopes and the pursuit guarantee are not covered under that limit. Pursuit bounds the evader’s thrust but leaves the pursuer’s unbounded.

Zero-order hold is checked at sample instants outside Lean. Among the cited pursuit champions, the Euler ranking does not survive this change of plant (§ 7.3). Inter-sample behavior and the validity envelope of the Clohessy–Wiltshire linearization remain uncovered. On the linear problems, Lean companions relate the certified updates to the stated Euler model and gain (Appendix § 11); they do not relate the discrete step to continuous dynamics.

Limitations of the evidence.

The campaigns cover three problems, only one nonlinear, with quadratic certificates on the linear pair. Each arm has twenty runs per base instance; the pursuit sweep and harder docking instances have ten. Spending caps leave Astra and Fable with fewer runs on one modified instance and none on the others.

We compare the four panel configurations at one effort setting, which gives different amounts of reasoning across models. Raising effort helps one tested model. We detect no benefit for the other. These controls do not isolate how reasoning effort contributes to the ordering between models. Astra and Sol were not swept over budget. In a prompt-only probe of 2 calls per setting, Astra uses a median of 4,283 output tokens at high effort against 2,470 at low; Sol shows no detectable change (5,678 against 6,160). Closed models are identified by alias and date rather than snapshot. The optimizer studies (§ 6.6) were limited to docking. They use two seeds and only seven of the sixteen optimizer and model combinations. Since model and effort change together, we cannot isolate their effects or fully explore how they interact with the optimizer. (Also, for the bound runs we used a proxy instead of $N$, so they cannot be as easily compared to the campaigns.) We would need more seeds, matched reasoning efforts, more combinations, a repeated-sampling baseline and direct optimization of $N$ for a fuller evaluation.

Correcting the standard baselines’ implementation weaknesses changes no conclusion (Appendix Table tab:baselines). The objective-aware optimizer closes most of the leading models’ advantage (§ 6.4). It remains local, and solver work is not equated with model inference; a stronger classical search is not excluded.

Astra proposes most of its linear-problem result immediately; Sol improves through later proposals and selection. Pursuit feedback helps Sol, but these runs do not pin down the effect’s size (§ 6.3). The experiments neither distinguish recall of the nominal design from reasoning nor explain the proposed Lyapunov shape. Saturation and noise certificates were completed after search. The recorded proof-repair attempts close two template-provable obligations when both a plan and an exact identity are supplied. All recorded attempts without the supplied identity fail, and the surviving records do not identify the failed step. In a separate experiment without a supplied plan, gpt-oss closes none of 11 obligations (§ 7.4).

On the linear problems, classical design with objective-aware certificates reaches scores close to the best models’. Establishing an advantage beyond these classical synthesis methods requires further evidence on nonlinear problems. SO(3) gives mixed evidence: no model detectably beats CMA-ES in the mixed design; Opus does when it writes every proposal, and one run exceeds the hand-tuned law while its median remains below it (§ 6.5). Full trajectory induction, torque saturation and switching logic remain to be tested.

The model or the optimizer.

The exploratory docking studies (§ 6.6) suggest that changing the model can improve results more consistently than changing the optimizer, but the setup is too limited for a general conclusion. Other studies also find that model and search procedure both matter, and that comparisons should account for computational cost [64, 55, 54]. In PCE the reliability of a result does not depend on either: the same certifying evaluator checks every candidate, however it was generated. Our isolation failure shows why this is not enough to protect the search environment. The checker can remain trustworthy while the proposer accesses earlier solutions (§ 7.5).

Implications for certification.

PCE produces explicit control laws with checked Lyapunov certificates. The kernel establishes the stated properties of the stated model. Comparisons between proposers still depend on statistical analysis, and applying a controller to a vehicle requires assessing the model’s fidelity. The language model remains a design tool; its execution is not part of the deployed controller.

Conclusion

PCE lets a language model search over controller and certificate parameters while returning an explicit law with checked guarantees. In the docking control, with the simulated-cost objective and mutation operator held fixed, 515 of 10,120 new proposals certify when selection retains certified candidates, compared with 0 without that rule. Subsequent certificate synthesis recovers 2 of 9,399 controllers (Table tab:filter).

The comparative results depend on the problem and search configuration. On the linear problems, the strongest models beat the standard baselines but do not clearly outperform classical design that also optimizes the certificate. The ranking among the cited pursuit champions does not survive zero-order-hold dynamics. On SO(3), no model detectably beats CMA-ES in the mixed search; Opus does when it writes every proposal, while its median remains below the hand-tuned law.

The recorded proof-repair attempts succeed in closing two template-provable obligations when both a plan and an exact identity are supplied; all recorded attempts without the supplied identity fail. Some failed attempts already contain that identity. The surviving records neither identify the failed step nor explain why the outcomes differ. In another experiment without a supplied plan, gpt-oss closes none of 11 obligations, with or without the identity. The exploratory docking studies show that the model can run the search as well, with the same exact checker deciding which designs are accepted. They also show why we need to isolate the search environment: a trustworthy evaluator does not prevent the model from accessing earlier solutions. We do not know yet whether model proposals improve synthesis in controller families with fewer classical methods and proof templates.

Acknowledgments

This work is supported by the Aerospace Corporation’s University Partnership Program, and partially by the Spanish Agencia Estatal de Investigación (AEI) under grant (ACTIVATION project) and by the Madrid Government (Comunidad de Madrid-Spain) under the Multiannual Agreement 2023-2026 with Universidad Politécnica de Madrid in the Line A, Emerging PhD researchers.

Problem and search specification

This appendix specifies the dynamics, parameter bounds, initialization, proposal rules and certificate checks used in the campaigns. These settings are taken from the implementation; Table 2 gives the campaign budgets. The certificate optimizer is described separately at the end.

Dynamics and controller parameters

Linear dynamics.

The state $z = (x, y, v_x, v_y)$ is in metres and metres per second, and one Euler step of $\Delta t = 1$ s of the Clohessy–Wiltshire equations with $n = 1.13\times10^{-3}$ rad/s gives $z^+ = Az + Bu$ with $A = I + \Delta t\,A_c$,

and $u = Kz$, unbounded except in § 7.1. The mission starts are $(1, 0.5, 0, 0)$, $(-0.8, 1, 0, 0)$ and $(0.3, -1.2, 0.01, -0.01)$; the speed limit has $\nu_0 = 0.2$ and $\nu_1 = 0.5$, the docking tolerance is $\left\lVert z \right\rVert \le 0.02$, and $K$ and $P$ are rationalized to fractions with denominators at most $10^4$. On pursuit the evader’s thrust is at most $0.01$ m/s$^2$ and the capture statement is at $1.5\,r_{\mathrm{cap}}$.

Attitude dynamics.

The inertia is $J = \operatorname{diag}(4.5, 5, 5.5)$ and $h = 0.1$ s. Both updates of a step use the current state: $R^+ = R\,(aI + h\hat\omega + b\,\omega\omega^\top)/d$ with $a = 1 - h^2\left\lVert \omega \right\rVert^2/4$, $b = h^2/2$ and $d = 1 + h^2\left\lVert \omega \right\rVert^2/4$, which is $R$ times the Cayley map of $h\omega$, and $\omega^+ = \omega + hJ^{-1}\bigl((J\omega)\times\omega + u\bigr)$, where the feed-forward term of $u$ cancels the gyroscopic term. The torque bound of Figure 2 is a certified output, the maximum of $\left\lVert u \right\rVert^2$ on $\{V \le c\}$ from a second linear program, not an imposed limit.

Genomes.

On the linear problems $K \in \mathbb{R}^{2\times4}$ has all entries free and $L$ is lower triangular; every proposed genome is clamped to $|K_{ij}| \le 5$, $|L_{ij}| \le 50$ and $L_{ii} \ge 10^{-3}$, so $P = LL^\top$ is positive definite. On SO(3) the genome is the fifteen diagonal gains of $\widehat G, G_c, M, C, K_\omega$ as positive rationals, rounded to denominators of at most 1000; a proposal with a non-positive gain is rejected, and there are no other bounds.

Initialization, selection and proposals

Seeded populations.

Each docking draw chooses one of the following:

• With probability 0.4, a gentle PD law with $k_p\sim U(0.001,0.02)$ and $k_d\sim U(0.03,0.25)$. Its certificate comes from the Lyapunov equation with $Q=\operatorname{diag}(q,q,1,1)$ and $q\sim U(0.001,0.1)$.

• With probability 0.3, a perturbation at scale 0.05 of LQR with $Q=R=I$.

• With probability 0.3, a random gain $K\sim\mathcal N(0,0.3^2)$ that passes tier 0, with a Lyapunov certificate for $Q=I$.

Failed draws are discarded and replaced, so the proportions in the accepted population can differ from the draw probabilities.

Pursuit starts from PD laws with $k_p\sim U(0.05,0.35)$, $k_d\sim U(0.3,1.3)$ and Lyapunov certificates for $q\sim U(0.05,1.5)$. Half the designs are then perturbed at scale 0.02.

SO(3) starts from isotropic geometric PD laws: $\widehat G=G_c=k_pI$, $M=J$, $C=\varepsilon I$ and $K_\omega=k_dJ$, with $k_p\sim U(0.6,1.4)$, $k_d\sim U(0.5,2)$ and $\varepsilon\sim U(0.12,0.35)$. These are the deliberately weak starts of § 6.5.

Selection and mutation.

On the linear problems, the elite contains six genomes. Runs with verification first retain the three best certified candidates, then fill the remaining places by score. Under the certified objective, every certified genome ranks above every uncertified one. Parents are drawn uniformly from this elite. The next population contains the elite, the model’s proposals, and enough Gaussian children to reach 28 members.

Each Gaussian child uses one of two operations, with equal probability:

• Perturb $K$ at scale $s_g$ and perturb $L$ at a relative scale.

• Perturb $K$ at the same scale and solve the discrete Lyapunov equation with $Q = \operatorname{diag}(q,q,1,1)$ and $\log_{10}q \sim U(-3.5,-0.5)$. If the modified loop is unstable, retain the parent’s $L$.

Both operations also zero one randomly chosen gain with probability 0.15. The mutation scale at generation $g$ is $s_g = 0.06\cdot0.88^g$ on docking and $0.05\cdot0.9^g$ on pursuit.

On SO(3), selection retains the twelve best certified angles from parents and children together; uncertified genomes score zero. The model sees the best four candidates. Gaussian mutation multiplies each gain by $\exp(\mathcal N(0,\sigma^2))$, with $\sigma=0.25\cdot0.92^g$.

Model calls and the ledger.

The model is called at generations $0, 3, \dots, 21$ on the linear problems and $3, 6, 9$ on SO(3), for eight candidates each time, and is shown the elite; a failed call is logged and replaced by Gaussian children. A proposal is a distinct genome; repeats are free and tier-0 rejects are charged. On the linear problems the loop arms offer at most 534 distinct genomes: the initial population contributes 28, and each of the 23 later generations adds at most 22, giving $23\cdot22=506$ new genomes and $28+506=534$ in total. Each classical arm receives the Gaussian arm’s spend on the same seed as its allowance. On SO(3), the allowance of 120 is enforced.

Certificate checks and objectives

Docking.

On docking, exact $LDL^\top$ bisection finds $\alpha$, $\beta$ and $\varepsilon$. The same test finds $\rho$, bracketed by the largest floating-point generalized eigenvalue; $1-\rho$ is rounded down to nine significant figures and confirmed exactly. The safety multiplier starts at 1.05 times its floating-point estimate, rounded up on a $10^{-6}$ grid. Up to four exact checks are tried, multiplying by $6/5$ after each failure. The docking bound is the smallest $n$ with $\rho^n c_{\mathrm{needed}}\le\alpha(0.02)^2$, verified exactly.

Pursuit.

A 33-point scan chooses $\rho_r$ to minimize $C_{\mathrm{cap}}$. Exact bisection on the S-procedure matrix finds $\mu$, and $r_{\mathrm{cap}}=\sqrt{C_{\mathrm{cap}}/\alpha}$.

SO(3).

The region level $c$ starts at $1/4$ and doubles up to eight times while the linear program certifies $\rho\le0.995$, followed by seven bisection steps. CVXPY with Clarabel uses a Gram dominance margin of $10^{-3}$ and two scaling rounds. Champions are re-verified at denominators $10^7$ and $10^9$, requiring the exact identity, exact diagonal dominance and $\rho\le0.995$. For Lean, the decrease program is re-solved with a sparsity penalty to shorten the file. Sol’s model-only champion uses the unpenalized solution because its penalized exact rate exceeded $0.995$.

Simulated cost.

The cost of § 6.2.4 is, over 1500 steps from each mission start,

where $h(z) = \nu_0^2 + \nu_1^2\left\lVert r \right\rVert^2 - \left\lVert v \right\rVert^2$ and $t_s$ is the smallest $t$ with $\left\lVert z_{t+1} \right\rVert < 0.02$ (1500 if there is none).

Classical certificate optimizer

The PD lattices are $9 \times 9$ on docking ($k_p \in [10^{-3}, 10^{-1}]$, $k_d \in [0.03, 1]$, each with and without the Coriolis cancellation) and $13 \times 13$ on pursuit ($k_p \in [0.02, 2]$, $k_d \in [0.1, 4]$), plus the gains of the seeded pool. Each certificate step tries twelve rates per gain, $1 - \rho$ geometric from $0.98\,(1 - \rho(A_{\mathrm{cl}})^2)$ down to $10^{-4}$, and the joint program on pursuit uses 33 rates with $1 - \rho$ geometric from $0.98$ to $10^{-4}$. The alternation runs ten rounds with restarts at scales 0.05 and 0.2, up to 20,000 solver calls (Clarabel, with SCS as fallback). Each fixed-rate program imposes the contraction at $\rho' = \rho - 10^{-3}(1 - \rho)$, and on docking it fixes the S-procedure multiplier at $\lambda_0 = \nu_0^2 (1 - 10^{-3})/1.05$, so that the exact completion, which pads the multiplier by 1.05, accepts the result.

Formal checking in Lean

For each cited design the certificate compiler writes a Lean 4 file [24] against mathlib [25]. On the linear problems each certificate condition becomes one polynomial identity, closed by ring, a statement that the squares of the $LDL^\top$ decomposition are nonnegative, and a chain of inequalities closed by linarith. The exact rational coefficients appear in the file as literal data, so the only search left to linarith is for a linear combination of facts the file supplies. No step requires a language model or an external solver. The templates supply the identities and inequalities that the tactics discharge. Elaboration turns these tactic scripts into proof terms, and the Lean kernel checks the terms; the mathlib lemmas they use are kernel-checked in the same way. The compiler and the tactics are therefore outside the trust base.

The docking and pursuit files state the closed-loop update using literal rational coefficients. These coefficients already combine the plant, time step and gain, so checking the certificate alone would not establish that the compiler used the intended model.

Each cited file therefore has a companion proof that states the mean motion, thrust gains, time step $\Delta t$ and gain $K$ separately. For every state component, it proves that the certified update equals $z_i+\Delta t\,f_i(z,Kz)$, adding $\Delta t\,b_iw_i$ on pursuit, where $f$ is the continuous-time Clohessy–Wiltshire field. The tactic ring checks these identities. An inconsistency between the stated model and the certificate’s coefficients fails the build. The companions are generated from the same run records and undergo the same audit as the certificate files.

An independent driver then calls Lean.collectAxioms on every declared theorem and requires its axiom footprint to lie within [propext, Classical.choice, Quot.sound], the three axioms of Lean’s standard foundations. Any other axiom is rejected, including sorryAx, which marks an unfinished proof, the axiom introduced by native evaluation, and any axiom the file declares. § 7.5 describes why the audit calls Lean directly rather than reading the build log. What the kernel does not check is whether the theorem states the intended property of the intended model: the theorem statements and the model assumptions require review (§ 8).

Proof-repair protocols.

The repair loop uses the Codex CLI coding agent at low reasoning effort; its underlying model version was not recorded. The model proposes a tactic block, lake build checks it, and compiler errors are returned for the next attempt. Success requires the project to compile, the number of open obligations to decrease, and the proposed block to contain no sorry. These obligations are already known to be provable by template. The model sees the reduced file and a proof plan written by the authors, so the experiment tests assembly of a supplied plan.

The separate gpt-oss experiment uses the following protocol. Each file retains definitions and statements but no proofs, preventing copying from neighbouring proofs or earlier repairs. Each obligation is attempted from the same file with and without its key identity from the generator. The model uses the panel’s low effort and 4 feedback rounds. Obligations, conditions and settings were fixed before any call.

Artifact provenance

The paper uses separate checks for formal guarantees, numerical certificate verification and empirical comparisons. Table 7 identifies the check behind each type of statement. A kernel-checked control theorem does not verify a campaign statistic or a simulated trajectory.

The command python -m tools.paper_tables --check checks the tables and numerical macros in against their recorded sources. The source paths are listed in , and records source and output hashes. Figures and their inputs are recorded in and checked by python -m tools.paper_figures --check.

Statement class	Checked by
Per-candidate control theorems: stability, safety envelope, safe_forever, docking within $N$; the strategy-quantified pursuit bound and trajectory-level capture; the nine-cell saturated decrease and its trajectory chain; the SO(3) step and regional decrease; template- or LLM-authored alike	Lean 4 kernel; footprint by an independent Lean.collectAxioms driver, a subset of [propext, Classical.choice, Quot.sound]
In-loop admissibility on the linear problems; step counts $N$; certificate completions; the stage rescoring of Table tab:stages; the re-verification of every SO(3) champion and the positive definiteness of its $V$	Exact rational arithmetic (Python Fraction)
Campaign medians, paired differences, bootstrap intervals, Wilcoxon and Holm $p$	Float statistics, recomputed from the run summaries before every release
Fitness, the SO(3) in-loop scoring, trajectories, attack results, session-log audits	Float simulation and forensics (unverified)

Certificates.

We cite 102 Lean files carrying 1535 theorems. The independent collectAxioms audit passed 102 files. The optimizer studies are not included in these counts. They add 44 champion files and 606 theorems from the 28 main runs, four supervised runs, six additional Opus runs and six GEPA pilots, two of them on pursuit. All these files passed the same kernel check and axiom audit. The archive contains 6 earlier champions with audited certificates, carrying 70 theorems. Its 3 genome reconstructions are marked as such. All paper quantities are generated from run records; the release gate rejects the record, table and PDF inconsistencies it checks.

Additional results

Interface-control protocol.

Astra’s CLI provides a read-only shell. In the execution-enabled variant, the model ran Python in 58 of 161 sessions, including 115 commands invoking scipy’s differential evolution. This computation was not charged to the proposal ledger. With execution disabled, live tool use was 0 of 160 calls, verified from the event stream.

Opus’s CLI ran in an empty directory with no tools, settings or stored session and used the required system line, Answer the user’s request.

Choice of the docking objective.

Preliminary runs used the proxy $\rho=1-\varepsilon/\beta$ with fixed floating-point padding, which can reverse the ranking obtained by directly certifying contraction (Table tab:stages). Exact bisection within the proxy formulation (Stage A) rescales the bounds almost uniformly by 2.24$\times$. Direct certification (Stage B) tightens them by a further 7–33$\times$ and reverses their order: the Gaussian design ranked last by the proxy beats its leading LLM design by 3.0$\times$. Every reported campaign optimizes Stage B; proxy rankings are not used. We used the padded proxy for the bound runs in the optimizer studies (§ 6.6). Figure 16 compares its results with Stage B across 22 docking-bound designs, including pilots and repeats.

Comparison families.

Docking compares each panel arm with full-allowance synthesis: 7 comparisons, fixed after the docking results.

Pursuit includes pairs involving a classical baseline, feedback controls against their arms, and one model pair, with a separate family per budget. Of 21 comparisons, 5 involve unreported models. Restricting Holm adjustment to the 16 reported pairs (Table tab:supppursuit and the gpt-oss feedback control) changes no decision at $p=0.05$. Including unreported pairs can only increase adjusted $p$.

SO(3) uses all pairs of the six campaign arms and a separate model-only family, both fixed in code before model calls. The API Opus arm occupies the campaign family under a rule fixed before its calls; model-only Opus is compared with its CLI mixed arm. Harder docking instances each have their own family.

Docking and pursuit families are outcome-informed and exploratory. Adjustment does not make them confirmatory.

Exclusion of degenerate runs.

Runs losing more than a quarter of model calls are excluded and archived. The rule preceded all five exclusions: one pursuit run, two SO(3) runs and two harder-instance runs. Every retained run lost at most a quarter; every excluded run lost at least a third. Any threshold from 25% up to, but excluding, one third gives the same exclusions.

Sensitivity checks recompute every comparison and family. At 20%, 14 additional runs losing exactly two of eight calls are excluded, affecting 44 of 173 comparisons. No median difference changes sign. Of 4 comparisons moving above $p=0.05$, 4 belong to the ten-seed instance families. With no exclusions, no median paired difference changes sign and one comparison moves below the threshold: high-effort Fable against Gaussian mutation on unequal thrust. None is interpreted as a detected difference.

Transfer of existing designs.

Table tab:transfer re-certifies existing designs without further search. It reports certified seeds and median best bounds for the initial population, the best of 2500 PD-grid designs with textbook repair, and certification counts and median bounds for archived base champions. The final rows give settings for which the initialization procedure found a certified starting population on only one of ten seeds.

Structure of the docking champions.

Astra approximately cancels Coriolis coupling in 20 of 20 runs. The Figure 6 gain is $K_{14}=-K_{23}=-0.00226$, close to $\mp2n=\mp0.00226$; the rationalized residual is $8.6\times 10^{-9}$. This decouples the loop into two nearly identical second-order systems. No Opus or gpt-oss champion has the cancellation.

Table tab:coriolis tests its value under Stage B by removing it from Astra designs, varying it on a fixed PD grid, and fixing it in Gaussian mutation. Removing it changes the median by about one step. The grid gives the same best bound with or without cancellation, both with Lyapunov repair and with a champion’s fixed $L$. Fixing cancellation in Gaussian search detects no difference.

The Lyapunov cross-term ratio tracks the docking bound in the rescored champions (Table 8). This association is exploratory, mixes arm and seed effects, and is not a causal measurement. The rescore excludes Sol and grid-bounded synthesis.

Population or statistic	Value
Seeded population: cross-term ratio	2.5
Gaussian champions: cross-term ratio	2.9
Synthesis champions: cross-term ratio	4.5
gpt-oss champions: cross-term ratio	3.5
Opus champions: cross-term ratio	3.6
Astra champions: cross-term ratio	6.3
Rescored champions	220
Rescored arms, including controls	11
Spearman correlation with the bound	$-0.83$
Champions with $N\le39$	70
Cross-term ratio of those champions	$6.0$–$6.9$

Baselines rerun.

Table tab:baselines compares each revised classical implementation with its original version. It reports the median certified docking bound or pursuit radius and the number of seeds that certify. The “vs recorded” columns count seeds where the revised version is better, worse or tied with the original. The “vs” columns compare it with the named reference arm. CMA-ES step scalings $0.1$ and $0.001$ are sensitivity checks on seeds 0–9.

Optimizer studies: further details.

The optimizer configurations are given in Table 9. All approaches submit genomes to the same external evaluator, but differ in how they organize the search and use model calls. The table records the engine versions, what each model call does and the stopping limits.

optimizer	implementation	per model call	stops at
GOA GEPA	GEPA 0.1.4 (PyPI), gepa engine	one reflection: reads a candidate and its feedback, writes one revision	reflections or 560 evaluations
GOA Meta-Harness	GEPA GitHub commit 48f1f65d, meta_harness engine	one agent session: reads all earlier candidates, may run code, writes up to 10	sessions or 560 evaluations
GOA Omni	same commit, optimize_best_of then optimize_sequential	as the engine running (GEPA, Meta-Harness, AutoResearch)	$3 \times 62$, then $2 \times 187$ evaluations; unused allowances are not passed on
prime-agent	prime-agent 0.9.7, autonomous mode	one agent turn in a persistent Python kernel, often submitting tens of genomes by script	evaluations, or a time or spending limit

Table tab:optall gives results and resources by arm; Table tab:optruns gives each run’s evaluation count, stopping reason and final result on the two axes. We include these details because not every optimizer reached the full evaluation budget, and using the same number of evaluations does not mean using the same inference cost.

We also tested a supervised variant of prime-agent with Sol 5.6, outside the two study axes. A supervisor could send one note after 80 evaluations without improvement, or when at least 30% of the previous 40 evaluations were rejected. The rejection condition was triggered in every run. Each note gave the rejection rate and remaining budget and reminded the agent that feedback identifies the failing check, without suggesting controller or certificate parameters. With supervision, cost was lower on one seed and higher on the other. The final bounds were 1,633 and 1,866, against 57 and 58 without supervision. With only two runs per objective, we cannot determine what caused these differences.

We also compare run time and resource use, and when each cost run first reached a certified design below 1 and 0.8 (Figure 17). This shows differences in how the approaches used their evaluation budgets beyond the final scores.

We show rejections by the first failing stage in the checker’s order in Figure 18. The original logs only give coarse verdicts, so we reconstructed the stages by re-checking designs from the 27 complete model runs and random search. For the model runs, the reconstructed stage agrees with the logged verdict in 14,492 of 14,501 evaluations; the remaining 9 are marked unmatched.

Supplementary material

Paired pursuit comparisons

Table tab:supppursuit reports the pursuit comparisons that include a classical baseline. For each pair, the difference is computed within seed as $r_A-r_B$, then summarized by its median and bootstrap 95% confidence interval. A negative difference favors A, because a smaller certified radius is better. The A / B / T column counts seeds where A is better, B is better, or the methods tie. The final columns give the unadjusted two-sided Wilcoxon $p$-value and its Holm-adjusted value. The comparison family is described in Appendix § 13.

Certificate optimization and thrust

Certificate optimization.

Table tab:suppcertopt compares the classical certificate optimizer with Astra and Sol. Differences are the optimizer’s value minus the model’s value, computed within seed. Both objectives are minimized, so a positive difference means the optimizer is worse. Wins, losses and ties are counted from the optimizer’s side. Holm adjustment uses the declared family across both problems.

Thrust demand.

Table 10 reports peak commanded acceleration per axis for the final designs. Simulated peaks use the docking mission starts and the pursuit fitness simulation’s worst-case evader. For docking, the table also gives the largest command anywhere in each certified set; this can exceed the simulated peak. The “$>u_m$” columns count designs whose peak exceeds the actuator limit $u_m=0.2$ m/s$^2$. These measurements concern the original unbounded-thrust designs; they do not establish performance with clipped thrust.

		simulated peak	certified-set peak
3-5(l)6-8 Problem	Arm	median	max	$> u_m$	median	max	$> u_m$
docking	Gaussian mutation	0.021	0.028	0/20	0.030	0.040	0/20
docking	CMA-ES	0.014	0.023	0/20	0.025	0.035	0/20
docking	alternating SDP synthesis (full allowance)	0.137	0.158	0/20	0.213	0.219	20/20
docking	Astra	0.026	0.048	0/20	0.061	0.094	0/20
docking	Sol	0.027	0.170	0/20	0.063	0.223	2/20
docking	Opus	0.030	0.077	0/20	0.041	0.101	0/20
docking	gpt-oss	0.022	0.057	0/20	0.037	0.101	0/20
pursuit	Gaussian mutation	0.475	0.539	20/20	–	–	–
pursuit	CMA-ES	0.513	0.634	20/20	–	–	–
pursuit	PD grid search	0.775	0.775	20/20	–	–	–
pursuit	Astra	0.918	0.918	20/20	–	–	–
pursuit	Sol	0.881	1.079	20/20	–	–	–
pursuit	Opus	0.864	1.097	20/20	–	–	–
pursuit	gpt-oss	0.470	0.598	20/20	–	–	–

Coverage of the guarantees

Table tab:coverage separates the guarantees established for each cited design. Each group names the dynamics model. Statements concern rationalized controllers and certificates over exact reals at sample instants. The columns have the following meanings:

The marks distinguish the evidence: “Lean” is a kernel-checked theorem in an audited file, “exact” is a rational check outside Lean, and “–” means the property is not covered. The guarantees in different columns are separate; for example, the table does not claim a combined noise-and-saturation theorem.

$^{a}$No thrust-limit certificate: no $\theta$ in the grid both covers the mission states and admits a sector multiplier. The cited designs of the other arms (4 on docking, 4 on pursuit, 2 on SO(3)) each carry the marks of a campaign row of their problem.