- full support for `upto` in verify/instance endpoints - "back-annotation facilities" as a way to trace the set of concrete calls to a function in unrolling
