A Gödel machine is an approach to Artificial General Intelligence that uses a recursive self-improvement architecture proposed by Jürgen Schmidhuber based of the mathematical theories of Kurt Gödel.
Schmidhuber’s design uses axioms to systematically search through its own code to find useful re-writes (which are deemed useful if they result in greater utility for the AI). The axioms include a detailed formal description of the machine's software and hardware, including both the components interacting with the environment and those dealing with the formal proofs, and a possibly partial description of the environment.
According to Schmidhuber this approach is globally optimal. This is because the machine has to prove that it is not more useful to continue the proof search for alternative self-rewrites.
The Gödel machine is often compared with Marcus Hutter's AIXI. Both are formal specifications of AGI. Schmidhuber points out that the Gödel machine could start out by implementing AIXI, and self-modify after it proves such a change is beneficial.