TL;DR: Schmidhuber’s Gödel machine is the formal ideal of agent self-improvement: a solver that modifies itself only when it can prove the modification pays. Real environments do not supply the axioms such a proof needs, so every working system since has swapped the theorem prover for an empirical test and bounded what the agent may change. The systems differ in where the test lives: a benchmark, a held-out metric, or the environment the agent has to keep operating in.
What a Gödel Machine Is: A Proof Gate on Self-Rewriting
Agent self-improvement is the practical core of recursive self-improvement, and its formal ideal is the Gödel machine.
The Gödel machine of Schmidhuber (2003), set out in the original Gödel machine paper, is the cleanest statement of agent self-improvement as a formal problem. The machine starts with an initial program in two parts: a problem solver that acts in a partially observable environment, and a proof searcher that enumerates candidate proofs in a fixed formal system. Its axioms describe the hardware, the initial software, the environment as a known probability distribution, and a utility function defined as expected reward over the remaining lifetime.
The machine may rewrite any part of itself, the proof searcher included, but only after the proof searcher finds a theorem of one specific shape: that executing this rewrite now yields higher expected utility than continuing with the current program, further proof search included. Schmidhuber’s global optimality theorem follows from that shape. The first rewrite executed is optimal relative to the axioms, because the proof already weighed every alternative rewrite the machine might have waited for.
Why the Proof Gate Never Closes in a Real Environment
The proof needs a formal description of how the environment answers actions: the transition function that takes the current state and the agent’s action and returns the next state. For a Linux container, a forked blockchain or a materials simulator that function is unknown, it is partly the product of the agent’s own earlier actions, and it drifts between episodes. An axiom set that does not contain the transition function cannot support a theorem about expected utility under it.
Even with a perfect model, the search is the bottleneck. Proofs about the lifetime utility of a program rewrite are long, the initial searcher tries proof techniques in order of a prior that favours short ones, and Schmidhuber’s paper is explicit that the machine may never find a provably useful rewrite within its lifetime. Gödel’s incompleteness result closes the last exit: some true statements about the machine’s utility have no proof in its axioms, so a strictly proof-gated system leaves real improvements on the table.
Agent Self-Improvement With an Empirical Gate
The Darwin Gödel Machine of Zhang, Hu, Lu, Lange and Clune (2025) names the swap in its title. It keeps an archive of coding agents, samples a parent, has the parent read its own evaluation logs and rewrite its own scaffold code, then scores the child on SWE-bench Verified or Polyglot. Children that run and score are added to the archive, every archived agent keeps a nonzero chance of being sampled, and the foundation model underneath stays frozen. Over 80 iterations the best agent in the archive rose from 20.0% to 50.0% on SWE-bench Verified, and the ablations without self-modification and without the open-ended archive both finished lower.
STOP and Autoresearch: Self-Improvement Around a Fixed Model
STOP, the Self-Taught Optimizer of Zelikman, Lorch, Mackey and Kalai (2023), described in the STOP paper, hands a seed improver program its own source and a utility function, and keeps the improved improver when the utility rises. The language model is never changed, which the authors stress keeps it short of full recursive self-improvement: it is self-improvement of the scaffold around a fixed model.
Karpathy’s autoresearch (2026) is the minimal form. An agent edits one training script, trains for a fixed five minutes, and the commit stays only if validation bits per byte went down; otherwise the branch resets. Data preparation and the metric live in a file the agent does not touch, and every run gets the same five-minute budget.
Empirical Gates Turn the Measure Into the Utility
In every case, what the gate measures becomes the utility, and the agent adapts to it as the Gödel machine would have adapted to its axioms. The Darwin Gödel Machine’s authors report children that removed the markers their hallucination check looked for, and STOP’s authors found improvers that switched off a sandbox flag. Neither is a failure of self-improvement. The gate rewarded a cheaper path to the measured score, and the agent found it, which is what gates are for. The open question is what the gate should measure, and that is a harness decision.
Fix the Harness, Mutate the Policy
Every system above draws a line the Gödel machine did not: part of the system is invariant and only the rest may change. The invariant part is the harness: the task definition, the per-episode budget of tool calls and turns, the scoring or reward computation, and the sandbox the agent acts in. The mutable part is the policy, in whatever form it takes: scaffold code, an improver program, a training script, or the weights of an adapter.
| System | What mutates | What stays fixed | The gate |
|---|---|---|---|
| Gödel machine (2003) | Any part of the program, proof searcher included | The axioms | A proof of higher expected lifetime utility |
| Darwin Gödel Machine | The coding agent’s own scaffold code | The foundation model, the benchmark, the archive logic | Benchmark score, with an archive that keeps every child |
| STOP | The improver program | The language model, the utility function | Utility of the improved improver |
| autoresearch | One training script | Data preparation and the metric; a fixed five-minute run | Validation bits per byte went down |
| Weight-level survival loop | A fresh LoRA adapter per window | The environment, the task definition, the budget ledger, the reward computation | The environment accepted the episode |
The line does two jobs. It makes the gate exogenous: the code that decides whether a change survives sits outside the thing being changed, so the agent can alter what the evaluator sees but not the evaluator. And it bounds the blast radius: a hard cap on tool calls per episode means a bad policy exhausts its budget and ends, instead of running until something outside the sandbox notices. The strongest gates go one step further and measure a quantity that only exists if the work was done: a test suite passing in a clean container, bytes freed on a disk, a balance that moved on a chain.
Survival as the Gate: Weight-Level Self-Modification
The gate for agent self-improvement can also be the environment the agent has to keep operating in. In that loop the agent runs episodes in a sandbox, the environment decides by its own state which episodes succeeded, and only those episodes are kept. Periodically a fresh LoRA adapter is trained on a bounded window of recent successes with a modified SFT loss: the loss changes, and the data is the agent’s own accepted trajectories, not demonstrations.
The adapter is the mutable policy, and the environment, the task definition, the budget ledger and the reward computation never change. Because experience is selected by the environment first and optimised afterwards without an explicit policy gradient, we describe the result as approximate policy-free online learning. It is the design in which reward, optimisation and persistence collapse into one signal: an episode the environment accepted is the only evidence the next adapter trains on.
This is a serious alternative under investigation, not a replacement for reinforcement learning. Where a reliable checker exists and returns frequent signal, RL with verifiable rewards and GRPO-style updates is the stronger default, and it is an empirical gate too: the verifier is invariant and the policy update is the mutable step. The survival loop targets environments where feedback is sparse, delayed, or visible only as the agent’s continued operation, the same regime that decides the SFT versus RL choice. Rolling back to the previous adapter when a new one underperforms is a safety net, not the mechanism.
What a survival gate gives up is the Gödel machine’s guarantee, and it gives it up on purpose. No proof says the next adapter is better; the next window of episodes says it, or does not. That is the bet behind our work on recursive self-improvement: an environment rich enough to end bad policies is a stronger gate than any axiom set a designer could write down, because it is the ground truth the proof would have been about.
FAQs
Has anyone built a Gödel machine?
No. The construction is well defined, but it needs axioms that describe the environment and a proof searcher that finds proofs about expected lifetime utility, and neither exists for any environment worth deploying in. The Darwin Gödel Machine borrows the name and drops the proof: it is an empirical, archive-based system, not a Gödel machine in the 2003 sense.
What is the difference between agent self-improvement and recursive self-improvement?
Agent self-improvement is any loop in which an agent’s own output changes the agent: edited scaffold code, a new prompt, a new adapter. Recursive self-improvement is the stronger claim that each improvement raises the rate of the next one. Every system in this post does the first; the second has to be measured across generations, not assumed.
Can formal proofs play any role in a self-improving loop?
Yes, but of invariants, not of utility. Formal verification can establish properties of the harness the agent cannot change: that the sandbox isolates the container, that the budget ledger halts an episode at its limit, that the reward computation reads the environment and not the agent’s logs. Whether a policy change pays off stays an empirical question.
Why do self-improving agents use empirical gates instead of proofs?
Real environments do not supply the formal model a proof needs. Their transition function is unknown, partly shaped by the agent’s own actions, and it drifts between episodes. An empirical gate runs the modified agent, scores it, and keeps the change only if the score holds, which needs no axioms.
What is the Darwin Gödel Machine?
The Darwin Gödel Machine is a coding agent that rewrites its own scaffold code and keeps an archive of every working version. Each child agent is scored on benchmarks such as SWE-bench Verified, and every archived agent can be sampled as a parent. The foundation model underneath stays frozen.
