We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

翻译：我们提出了一种自动化框架，用于在编译时强化软件规约、其依赖类型模型与实现之间的内聚性。模型检测与类型检测目前是自动验证程序正确性的两种独立技术。通过利用基于属性的测试、索引状态单子与依赖类型，我们能够对多个有趣的系统与网络协议进行建模，使类型检查器验证我们的实现是否符合规约，并测试模型是否匹配规约的语义；这是迈向结合模型检测与类型检测的一步。