This work is a case study of the formal verification and complexity analysis of some famous probabilistic data structures and algorithms in the proof assistant Isabelle/HOL: – the expected number of comparisons in randomised Quicksort – the average-case analysis of deterministic Quicksort – the expected shape of an unbalanced random Binary Search Tree – the expected shape of a Treap The last two have, to our knowledge, never been analysed in a theorem prover before and the last one is particularly interesting because the analysis involves continuous distributions. The verification builds on the existing probability and measure theory in Isabelle/HOL. Algorithms are shallowly embedded and expressed in the Giry monad, which allows for a very natural and high-level presentation.