The type of transformations that AST uses are syntax-based rewrite rules whose application is fully automatic. Oftentimes, small transformations tend to be highly reusable with respect to a specific problem domain.
Correctness proofs are generally managable for small transformations.
Correctness In AST, transformations are given a formal semantics via an extended denotational semantic framework. Given an expression describing the semantics of a transformation, an automated reasoning system can be used to verify the correctness of that transformation. If you haven't done so already, please read Sandia's disclaimer .