Here is the latest (pdf) version of the formalization (within set theory) of the idea of a self-constructing mathematical universe. The axioms are presented along with a schema for generating candidates to satisfy the axioms; the main necessary condition for a forcing set to succeed in this schema is derived.