Many results of persistence of quasi-periodic solutions (Kolmogorov, Arnold, Moser theory) can be recast in a-posteriori format. That is, given an approximate solution of an invariance equation, there is a true solution close to it. There are many applications of these a-posteriori format. Notably, one can take as approximate solutions the results of a numerical calculation. Hence obtain results of the constants in concrete examples which are more than 99% of other rigorous upper bounds. One can also take as input of an a-posteriori theorem the results of formal expansions. One then gets differentiability. Some more recent developments are that one also obtains results on Whitney differentiability with respect to the frequency. This allows to prove the results in near integrable systems with very weak non-degeneracy assumptions and to give very sharp characterizations of analyticity domains.