This paper documents a computer-assisted procedure for rigorously analyzing small hyper-bolic 3-manifolds. Briefly, we will define a compact six-dimensional space P that parame- terizes pairs of elements of Isom(H3 ), and then construct a regular binary space partition (BSP) tree which subdivides P into subregions Pi and whose leaves are — with a few ex- ceptions — labeled with killerwords. These killerwords will encode miniature proofs that Pi cannot contain any points which correspond to particular choices of pairs of generators of any torsion-free discrete group of Isom(H3 ). This tree of mini-proofs will then be used to ex- haustively isolate all possible manifolds which can have properties related to the dimensions of P. This method has been used as a foundation for tackling multiple long-standing problems at the interface of hyperbolic geometry and low-dimensional topology. In particular: topo- logical rigidity of hyperbolic 3-manifolds; the generalized Smale conjecture for hyperbolic 3-manifolds; finding the closed 3-manifold of least volume; and the Gordon conjecture on exceptional Dehn fillings.