Higher-order logics are expressive tools for tasks ranging from formalizing the foundations of mathematics to large-scale software verification and synthesis. Because of their complexity, proofs in higher-order logics often use a combination of interactive proving together with computationally-intensive tactic applications that perform proof automation. As problems and proof automation become more sophisticated, these proofs represent substantial investments---each interactive step may represent several hours of design time.
We present an implementation of a distributed proving architecture to address the problems of speed, availability, and reliability in tactic provers. This architecture is implemented as a module in the MetaPRL logical framework. The implementation supports arbitrary process joins and all-but-one process failures at any time during a proof. Proof distribution is completely transparent; the existing tactic base is unmodified.