BIOPS first invokes a variant of Levin's universal search  (Levin attributes similar ideas to Adleman ). Universal search is a simple, asymptotically optimal [22,24,25,16,48], near-bias-optimal [38,40] way of solving a broad class of problems whose solutions can be quickly verified. It was originally described for universal Turing machines with unlimited storage . In realistic settings, however, we have to introduce a recursive procedure [38,40] for time-optimal backtracking in program space to perform efficient storage management on realistic, limited computers.
Previous practical variants and extensions of universal search have been been applied [33,35,45,38,40] to offline program search tasks where the program inputs are fixed such that the same program always produces the same results.
This is not the case in the present online setting: the same proof technique started at different times may yield different proofs, as it may read parts of (such as the inputs) that change as the Gödel machine's life proceeds. Nevertheless, we may apply a variant of universal search to the space of proof-generating programs as follows.
For convenience, let us first rename the storage writable by proof techniques: we place switchprog, proof, and all other proof technique-writable storage cells in a common address space called encoded somewhere in , with -th component . To efficiently undo temp changes, we introduce global Boolean variables (initially FALSE) for all . In the method below we notationally suppress the task dependency seen in Def. 2.1:
Make an empty stack called Stack. FOR all self-delimiting proof techniques satisfying DO:
None of the proof techniques can produce an incorrect proof, due to the nature of the theorem-generating instructions from Section 2.2.1. A proof technique can interrupt Method 2.1 only by invoking the instruction check() which may transfer control to switchprog (which possibly will delete or rewrite Method 2.1).
Clearly, since the initial runs on the formalized hardware of the Gödel machine, and since proof techniques tested by can read and other parts of , they can produce proofs concerning the (expected or worst-case) performance of itself.