We are using interval arithmetic to implement derivations of rigorous bounds on the length spectrum of hyperbolic three-manifolds. Our current task is deriving a positive lower bound on the systole length.