Delegation is a common programming idiom, whereby a task is carried out by a delegate---a procedure that is typically not known statically. Delegation enhances the modularity and the extensibility of a program, and, therefore, is the main ingredient of many design patterns such as Command, Chain of Responsibility, Visitor, and others. However, the dynamic nature of delegation complicates specification and verification, because the behavior of a client of delegates should be described in terms of the behavior of the statically-unknown delegates. Moreover, the specification of the client may actually depend on itself, through references to delegates: this is the well-known recursion through the store phenomenon. Recursion through the store is a problem because it is statically unpredictable and because it might introduce inconsistencies in a naïvely designed system. Most existing solutions to this problem apply higher-order logic, which is not amenable to automatic theorem proving. We present an expressive specification and verification methodology that enables automatic reasoning about delegation in first-order logic using SMT solvers. Our system introduces a simple and expressive way to handle recursion through the store. It also deals with features like state capturing, which involves abstraction and framing of the captured state. Our methodology has been proven sound. We demonstrate its expressiveness by specifying several examples and verifying them automatically in the Boogie program verifier.