Formal methods are recommended for the development of software controlled safety critical systems because they support formal verification. However, they raise the issue of validation. Mostly due to poor readability of formal texts, validation is difficult. The key idea of stepwise development process, such as B method is to break the general verification into a sequence of smaller steps, called proof-obligations, associated with each refinement. We aim at “breaking” validation in the similar way. Technology allows us to animate specifications so users can validate them. Verification and validation impose very different constraints on the specification text: the former prefers abstract, non constructive, legible (for specifiers!) texts, the latter requires concrete, constructive, computable texts, for instance. These constraints come from the processes (proofs) or the tools (provers, animators). Validation through animation implies to modify the text: using it on each refinement therefore requires a cost-effective transformation technique.