Transaction-level modeling (TLM) has been proposed as the leading strategy to address the ever-increasing complexity of digital systems. However, its introduction brings a new challenge for designers and verification engineers. Because no tools are available to automatically derive an RTL implementation from a transaction-level (TL) design, manual refinements are necessary. This article presents a hybrid, incremental assertion-based verification (ABV) methodology to check the correctness of the TL-to-RTL refinement. The methodology relies on reusing assertions and already-checked code and is guided by assertion coverage metrics.