The Bernays-Schonfinkel-Ramsey class is a classical decidable fragment of first-order logic, also known as EPR (effectively propositional reasoning). This fragment is decidable, and allows very restricted quantifier alternations. In spite of its apparent limitations, it has been successfully used for verification of heap manipulating programs in the doctoral research of Shachar Itzhaky, and more recently for verification of challenging distributed protocols in my doctoral research, both under Mooly’s supervision. Using EPR brings benefits of decidability and a finite model property, ensuring that either a proof or a finite counterexample can be obtained automatically. The fact that a logic as weak as EPR is useful for nontrivial verification tasks is quite surprising. In this talk I will review the ideas that make it possible to use EPR for verification of both heap manipulating programs and distributed protocols, and present some of the open questions this line of work raises.