Two papers were accepted at the Dafny 2024 workshop. The paper “Caesar: A Verifier for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski (Saarland University and UCL), Joost-Pieter Katoen and Christoph Matheja (TU Denmark) presents a quantitative program verification infrastructure for discrete probabilistic programs, building on our work published at OOPSLA 2023. The paper “Generation of Verified Assembly Code Using Dafny and Reinforcement Learning” by Christopher Brix and Jean-Baptiste Tristan (Amazon Web Services) is about how Dafny is integrated into a reinforcement learning process to generate efficient and correct assembly code.