We present VMC, an open-source Dafny library for verified randomized algorithms of the Monte Carlo type. Currently, VMC offers a range of verified samplers of standard distributions that can be used in Dafny, C#, and Java code. Each sampler consists of three parts: i) a functional model that transforms bitstreams to values in the domain of the desired distribution; ii) a proof that the functional model has the desired distribution; iii) an imperative implementation that uses external random bits as primitive and is proven equivalent to the functional model. Taking the uniform distribution as an example, we present each step in detail, report on the current status of the project, and discuss future work.