In this talk I will survey some of our work verifying implementations of distributed systems in the Verdi framework and discuss challenges in proof engineering we hope to address to expand the set of systems that can be effectively verified with proof assistants.