Bisimilarity of two processes is formally established by producing a bisimulation relation, i.e. a set of pairs of process expressions that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations to exhibit while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques make defining candidate relations easier and they significantly reduce the amount of work in proofs. Furthermore, they are increasingly becoming a crucial ingredient in the automated checking of bisimilarity. In this talk, we present our experience in using the Abella theorem prover for the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the pi-calculus. Our formalization is based on recent work on the proof theory of least and greatest fixpoints for accommodating the heavy use of coinductively defined relations and coinductive proofs about such relations. An important feature of our formalization is that our definitions and proofs are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. The presence of binders, as in the pi-calculus, is notoriously a delicate aspect to treat in formal proofs but we show that the underlying proof theoretic foundations of Abella makes it possible to smoothly lift the results from CCS to the pi-calculus. This is thanks to the use of lambda-tree syntax and generic reasoning through the nabla quantifier.