Promises and Challenges in Bridging TLA+ Designs with Implementations