Integrating Topological Proofs with Model Checking to Instrument Iterative Design