In this talk, I will first present my PhD subject, where, together with Arnaud Sangnier and Nathalie Sznajder, we studied networks with unboundedly many agents, each of them executing a protocol given as an automaton. They communicate via broadcast and non-blocking rendez-vous, and I will talk about three verification problems we studied during the PhD. One of the main contribution of my PhD is the introduction of a structural restriction on the shape of the protocols called Wait-Only, where each state of the protocol is either an action state (from which a process can only send messages) or a waiting state (a state from which it can only receive messages). We will see how this restriction gives significantly better complexity results for different verification problems, and why. I will then explain how my current postdoc subject also fits this quest of verifying distributed systems, although it takes a different approach, as it focuses on stateless model checking. I will explain the challenges and open questions in that area.