Algebraic effects and handlers provide a modular way to structure programs with computational effects and are increasingly adopted in practical programming languages such as OCaml. Their expressivity and utility stem from the capability to manipulate delimited continuations. However, delimited continuations also introduce complex control flows, making program verification more challenging.

In this talk, we present two complementary approaches to verifying programs with algebraic effects and handlers. Both approaches are based on Answer Type Modification (ATM), which enables type systems to precisely track what effects occur and in what order during program execution, reflecting this information as modifications to the answer types of delimited continuations. However, they use ATM in different ways.

The first approach introduces a novel dependent refinement type system for algebraic effects and handlers. This system incorporates a mechanism called Answer Refinement Modification (ARM), which can be seen as a specialization of ATM that applies modifications to the refinement predicates of answer refinement types. We automate refinement type checking and inference for the system by reducing them to solving Constrained Horn Clauses (CHCs) and integrating with existing CHC solvers, and have implemented this approach in RCaml, a refinement type-based verifier for OCaml.

The second approach extends higher-order model checking (HOMC) to programs with algebraic effects and handlers. While HOMC achieves decidability for pure higher-order programs with finite data domains, simply adding algebraic effects and handlers makes model checking undecidable due to the potential for an unbounded number of active handlers. To address this, we propose restricting programs using ATM, thereby bounding the number of active handlers. Under this restriction, the model checking problem becomes decidable again while still supporting a wide range of practical effects. To enable reuse of existing HOMC tools for pure programs, we present a CPS transformation that reduces the model checking of programs with algebraic effects and handlers to that of pure programs. We have implemented this approach in EffCaml, a transformation-based verifier for OCaml, which incorporates a type inference algorithm for our type system with ATM, the CPS transformation, and integration with HOMC tools.