In section 6.1 you mention experimenting with bypassing the precondition checks for correct-by-construction generators. Have you considered giving this "unsafe" runner a type that demands a completeness certificate for the generator (in the style of https://dl.acm.org/doi/10.1145/3158133) so that this optimization is at least available only when proven sound?