Cybersecurity in OT environments is challenging, due to persistent threats and legacy systems using outdated protocols. Formal methods can verify protocol correctness, but their assumptions often fail to appear in system design. We propose a methodology that maps protocol specifications to architectural assets and simulates attacker behavior to test these assumptions. Applying our approach to a real OT use case shows how evolving infrastructure can break initial assumptions and create new risks. Simulations reveal attacker paths and support targeted mitigations, aligning formal verification with real-world resilience through an iterative process.