Gain confidence in system correctness using formal and semi-formal methods - Ankush Desai

Ankush is a Principal Applied Scientist at AWS and is deeply interested in building tools and techniques that help developers build reliable systems. He’s one of the creators and the lead developer of the P programming framework for formally modeling and specifying complex distributed systems. His mission is to promote adoption of formal methods in all phases of the development cycle. The software industry loves the idea of “Shifting left” to find bugs as early as possible and formal methods are the ultimate “Shift left.” They force the developers to spend time thinking deeply about what they are building. Developers are often skeptical about formal methods as a software engineering practice, but it’s fascinating to see the parallels between property-based testing and formal methods. In essence, they both need to define what the system is and should do and validate that hypothesis. In his BugBash 2025 talk, Ankush softens the edges between formal methods and software testing by painting them as a thinking tool. Thinking eliminates a lot of the bugs in the design phase itself before even implementing the system. So borrowing ideas from formal methods and integrating them into the development process can bring a lot of value. While we at Antithesis already use semi-formal methods for the critical components of our infrastructure, we hope more people will spend more time thinking about their systems too. https://antithesis.com/blog/2025/bugb...