Software verification is a complex problem, and verification tools need significant tuning to achieve high performance. Due to this, many verifiers choose to specialize on basic reachability properties. Instead of implementing algorithms for each possible specification, some verifiers implement known transformations from the given specification to reachability on their internal representations. Unfortunately, those internal transformations are not reusable by others. To improve this situation, we propose TransVer, a tool which offers transformations as modular stand-alone component, modifying the input program instead of the internal representation, enabling their usage as a preprocessing step by other verifiers. This way, we separate two concerns: improving the performance of reachability analyses and implementing efficient transformations of arbitrary specifications to reachability. We implement the transformations in a framework that is based on instrumentation automata, inspired by the BLAST query language. In our initial study, we support three important concrete specifications for C programs: termination, no-overflow, and memory cleanup. We conduct experiments with ten different verifiers. The experiments evaluate the efficiency and effectiveness of our transformations. The results are promising: Our transformations can extend existing verifiers to be effective on specifications for which they have no integrated support, and the efficiency is often similar or better to state-of-the-art verifiers that have integrated support for the considered specifications.