The actor model is a well-established way to approach to modularly designing and implementing concurrent and/or distributed systems, seeing increasing adoption in industry. But deductive verification tailored to actor programs remains underexplored; general concurrent logics could be used, but the logics are complex and full of features to reason about behaviors the actor model strives to avoid.

We explore a relatively lightweight approach of extending a system for proving {sequential} program correctness with means to prove safety properties of distributed actor programs (currently, assuming no faults). We borrow ideas from hybrid logic, a modal logic for stating assertions are true at a particular point in a model (in this case, a particular actor’s local state). To make such assertions useful, we stabilize them using rely-guarantee-style reasoning over local actor states, and only permit sending stable versions of these assertions to other actors. By carefully restricting the formation of assertions that a proposition is true at a certain actor, we avoid the need for actors to handle each others’ rely-guarantee relations explicitly.

We find that almost all of the required restrictions either fall out of established reference immutability techniques or can be implemented as a Dafny library, and outline the minor additional extensions that would be required for a sound implementation. We use this library to verify an actor variant of a classic rely-guarantee example (lower-bounding a montonic counter).