Many distributed systems involve interactions among computers controlled by different parties. These systems must work correctly even when some of the participants are malicious and try to interfere with the system. In computer science , these kinds of malicious participants are called Byzantine participants. Various protocols and algorithms have been developed to ensure that the systems operate correctly so long as only a small fraction of the participants behave maliciously. However, implementations of these kinds of systems often have bugs. One class of bugs that is particularly challenging to address is liveness bugs, in which the system stops making progress and fails to complete operations. To reduce the incidence of bugs, researchers have developed an approach called formal verification, in which a mathematical proof is constructed that shows a software system is free from a certain class of bugs. However, existing methods for verifying the absence of liveness bugs have limitations that make them inapplicable to many important systems. This project develops new techniques for verifying the absence of liveness bugs in systems with malicious participants, expanding the kinds of systems that can be verified. In addition, the research team develops new tutorials, labs, and lectures on verification of distributed systems, and organizes the annual New England Systems Verification Day, which brings together verification researchers and industry practitioners. This project