We consider the problem of automated safety verification for distributed systems written using the actor model. The infinite state space of these systems prevents techniques such as symbolic execution or model checking from reaching a fixed point, leaving manual verification as the state-of-the- art. We propose a separation logic for actors extended with message histories recording the trace of messages handled during execution. During execution, we observe that these histories contain cycles for many common algorithms like Paxos, and this cyclic history is the cause of non-termination in prior techniques. We formalize requirements for soundly over-approximating these cyclic message histories, allowing for sound automated verification of safety properties via goal-directed abstract interpretation. Our techniques allow Paxos to be automatically proven safe without user-specified inductive invariants for the first time.