  Derandomization techniques are often used within advanced randomized
algorithms. In particular, pseudorandom objects, such as hash families and
expander graphs, are key components of such algorithms, but their verification
presents a challenge. This work shows how such algorithms can be expressed and
verified in Isabelle and presents a pseudorandom objects library that abstracts
away the involved deep algebraic/analytic results. Moreover, it presents
examples that show how the library eases and enables the verification of
advanced randomized algorithms. Highlighting the value of this framework is
that it was recently used to verify the optimal-space distinct elements
algorithm by Blasiok from 2018, which relies on the combination of many
derandomization techniques to achieve its optimality.
