In recent years, large-scale verification of industrial-strength software has become increasingly 29 common [52] following the inspirational success of CompCert [38] in Coq, or CakeML [32] in 30 Isabelle/HOL. However, such developments still require a tremendous amount of expertise 31 and efforts. A significant body of work hence seeks to simplify this task, whether through 32 richer semantic foundations [6, 11], or through richer proof principles [29, 56, 63]. 33 In the Coq ecosystem, the Interaction Trees (ITree) library by Xia et al.[58, 59] has 34 been influential over the recent years as a rich semantic toolbox for modelling first order 35 languages. Inspired by advances in denotational semantics [8, 18, 47], the library provides 36 an implementation of a coinductive variant of the freer monad [28]. This library provides 37 access to monadic programming over symbolic events, tail recursive and general recursion, 38 and interpretation of effects into monadic transformers in the style of one-shot algebraic 39 effects. Concerning proofs, a rich theory of weak bisimilarity of computations enables both 40 equational reasoning, and relational Hoare-style program logics. The approach has been 41 used to model and verify a wide range of applications, such as networked servers [30, 62], 42 transactional objects [39], non-interference [55], or memory-safe imperative programs [19]. 43