Kropf's group has performed a lot of interesting work on verification based deductive hardware design. Their recently designed class of handshake circuits with nice modular correctness properties seems suitable for transformational design as well. In particular, they seem to offer a possibility of integrating high-level transformation from predictive/functional specifications to tail recursive formulations with a compilation scheme from there into handshake circuits. Kropf's group is currently investigating optimising transformations that remove most of the overhead the handshake circuits introduce to guarantee the nice structural correctness properties. It was agreed that Augsburg and Karlsruhe will cooperate on integrating transformations and verification in this setting.