What's my type? Examining how model checking and type systems may complement and help each other.

Various different techniques, from type theory and model checking to numerous testing approaches, all try to achieve the same goal: verifying that software is correct. Yet all these disciplines tend to operate independently, rather than leveraging each other to handle their individual limitations. We have developed a unified framework for using different verification techniques in the same language, moving along this 'Spectrum of Verification' as necessary, thereby enabling a more granular approach to software verification. Real-world protocol implementations have been identified and we are working on showcasing this new approach using the implementations as examples where specification, verification, and implementation live alongside each other rather than as separate parts.