In his dissertation at the ETH Zurich Fahrad Mehta describes how theorem proving can be a practical tool for software engineers and presents the ideas that are used in building Rodin’s infrastructure.