VMC: a Dafny Library for Verified Monte Carlo Algorithms
summary
Open-source Dafny library that provides verified Monte Carlo samplers: each sampler has a bitstream-to-value functional model, a machine-checked proof that the model yields the claimed distribution, and an imperative implementation proven equivalent to the model and callable from Java/C#. Implements a verified Bernoulli-exponential sampler that yields probability e^{-γ}, proves it by formalizing limits and series, models nontermination via a probability monad with divergence and uses bounded-fuel limits to lift correctness to unbounded loops; parts remain axiomatized.
AI-written summary · about