This survey examines the challenges of developing high-confidence software for implantable medical devices, especially under closed-loop interaction with patient physiology. Using pacemakers as a running example, it outlines modeling, verification, abstraction, code generation, and testing techniques that help carry safety properties through the full design toolchain.