What is the state of the art in theory of "Software transformations preserving behavior"?
I think what you are looking for, in the context of verified transformations in a proof assistant, is known as "refinement", wherein a very-high level, inefficient implementation of some algorithm is gradually refined down into an efficient, low-level implementation, proving that the transformations preserve certain properties along the way.  Various tools have been developed to help the user do this without being overcome by tedious book keeping.

In terms of the state of the art, I think Lammich's tool in Isabelle/HOL has been used successfully in at least two significant developments (a verification of Hopcroft's algorithm by Lammich and Tuerk, and a verified implementation of an LTL model checker by Esparza, Lammich et al).  Ironically, I was also reading this paper this morning, about a similar tool, newly developed, in Coq, courtesy of the dependent_types subreddit on Reddit.