Professor Lesani received the NSF CAREER award for his work on "Distributed System Synthesis on Certified Middleware". Distributed systems are the backbone of modern computing. However, they are complicated and prone to bugs due to their combinatorially large state-spaces, and node and network failures. The inherent complication is faced by not only protocol and system designers that provide interfaces but even distributed application programmers that use these interfaces. This project includes both novel automatic synthesis techniques for client applications and novel verification techniques for distributed middleware.