Current mainstream programming/verification tools are not well-suited to build safe and secure distributed programs that meet required specifications. This is a serious issue because our modern society came to heavily rely on complex and constantly evolving distributed systems that need to tolerate all kinds of threats and attacks in order to protect critical and sensitive resources. This issue is due in part to the lack of formalisms, tools, and reliable foundations. Indeed, in the past few decades, we have seen a spurt of verification tools that handle well functional sequential code, but expressive tools to reason about distributed programs are only just emerging. Moreover, a major issue with such verification tools is that they are often very complex themselves, making them error prone.

In this talk I will present some of my contributions to this area, namely, I will present my work on (1) designing formal verification tools to reason about complex distributed systems (such as Byzantine fault tolerant consensus protocols as used in Blockchain technology); and (2) on ensuring that those verification tools rely on correct foundations.

I will conclude by showing how I believe distributed systems will have a positive impact on modern foundational/logical frameworks, and vice versa.