Software bugs can have disastrous consequences, ranging from financial costs to loss of human life. As a result, for high-stakes systems, software vendors are increasingly applying techniques that can prove the absence of various kinds of bugs. However, existing techniques have limitations that make them inapplicable for certain types of programs that make use of randomness, which is common in sensitive software domains such as cryptography and machine learning. This project will develop new techniques for reasoning about randomness in programs, which will make it possible to prove important properties about these programs, thereby improving software quality in these critical areas. In addition, the team of researchers will develop educational materials to make the project's ideas more broadly accessible to students, researchers, and industrial practitioners. This project targets programs that exhibit two important kinds of effectful features: concurrency and randomization. Existing formal verification techniques cannot handle the complexity and expressivity of many programming language features, and these features make it harder to write, test, and reason about programs. Establishing correctness in the presence of just one of these features is hard enough, and it only becomes more difficult when they are combined. This project will develop program logics and reasoning tools that can enable more precise, compositional analysis of concurrent randomized programs by building