Distributed protocols underlie more and more applications, making their correctness paramount. However, due to the infinite state space (e.g., unbounded number of nodes and messages) and the complexity of the protocols used, verification of such protocols is both undecidable and hard in practice.

A common practice is to model a program and its invariants using logical formulas. A major hurdle for verification of distributed protocols is the fact that they often require quantified inductive invariants, making the check of the verification conditions, let alone the inference of inductive invariants, difficult. This talk will discuss recent approaches for verifying distributed protocols by utilizing decidable fragments of first-order logic that are supported by leading satisfiability solvers and first-order theorem provers. Our experience shows that for verification conditions expressed in these fragments, solvers not only converge fast, but also behave quite predictably. We discuss approaches ranging from deductive verification, where the candidate inductive invariant is provided, to automatic inference of quantified invariants, through interactive inference.