We formalize the classical complexity classes $\mathrm{L}$, $\mathrm{NL}$, $\mathrm{P}$, $\mathrm{NP}$, $\mathrm{coNL}$, $\mathrm{coNP}$, $\mathrm{PSPACE}$, $\mathrm{NPSPACE}$, and $\mathrm{EXPTIME}$ for languages of finite binary strings. The definition of P is exactly that of lax-554803. NP uses polynomially bounded certificates and polynomial-time verification; EXPTIME uses the finite single-tape machines of that submission. The space classes use finite Turing machines with a bounded, read-only input tape and a separate work tape, whose space is bounded on every computation branch. We prove elementary containments, complementation identities, and the injectivity and linear length of the certificate encoding.