Type-level Property Based Testing

TL;DR

The paper addresses ensuring correctness for stateful, real-world systems by unifying specifications, dependently typed models, and implementations within Idris2 using type-level QuickCheck. It develops a framework that links the model, its implementation, and its test suite through Indexed State Monads (ISMs) and a Traceable interface, enabling compile-time verification of state transitions and trace properties. The ATM example demonstrates how dependent types encode stateful transitions and how QuickCheck can reveal modelling errors, which can then be fixed by refining the state representation (e.g., adding a PIN retry counter) and re-verifying. The approach is generalised to arbitrary stateful systems, demonstrated with an ARQ network protocol, and argues that this methodology provides fast feedback, avoids translation errors, and supports scalable testing of complex DSLs without resorting to external model checkers. Overall, the work shows how type-level, property-based testing can co-evolve specifications, implementations, and their semantics, potentially accelerating verification and prototyping in safety- and security-critical domains.

Abstract

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.

Figures (1)

• Figure 1: Diagram of the atm state machine