Bayesian analysis consists of modeling and inference as separate steps, where inference in turn consists of the conceptually separate steps of conditioning and querying. While probabilistic programming systems successfully decouple modeling from inference, they fail to decouple conditioning from querying. In this proposal we aim to formally specify a conditioning transformation that is verifiable, reusable, and useful. To this end we propose a set of semantics that aid in formally specifying conditioning, use the specifications to develop a robust algorithm and implementation of a conditioning tool, and reuse the tool on realistic applications involving MCMC samplers.