We study the extension 123) of the theory S21 by instances of the dual weak pigeonhole principle for p-time functions, dWPHPx2x. We propose a natural framework for formalization of randomized algorithms in bounded arithmetic, and use it to provide a strengthening of Wilkie's witnessing theorem for S21+dWPHP. We construct a propositional proof system WF , which captures the Π1b-consequences of S21+dWPHP. We also show that WF p-simulates the Unstructured Extended Nullstellensatz proof system of Buss et al. 256). We prove that (...) dWPHP is equivalent to a statement asserting the existence of a family of Boolean functions with exponential circuit complexity. Building on this result, we formalize the Nisan–Wigderson construction in a conservative extension of S21+dWPHP. (shrink)