We use Goedel's self-reference trick to build a universal problem solver. A Goedel machine is a computer whose original software includes axioms describing the hardware and the original software (this is possible without circularity) and some formal goal in form of an arbitrary user-defined utility function (e.g., cumulative future expected reward in a sequence of optimization tasks). The original software also includes a proof searcher which uses the axioms to systematically make pairs ("proof", "program") until it finds a proof that a rewrite of the original software through "program" will increase utility. The machine can be designed such that each self-rewrite is necessarily globally optimal in the sense of the utility function, even those rewrites that destroy the proof searcher. We relate the approach to previous asymptotically optimal search algorithms.