I wanted to learn formal verification with TLA+, but then I read that Alloy would be a better start. So here it is, Alloy 6. Install from https://github.com/AlloyTools/org.alloytools.alloy/releases

Let’s run a hypothetical example. We have a messaging system. We have coded this system well and all our tests are passing. But somehow we wonder if there is something we missed. It’s hard to know what we don’t know, right? Formal verification to the rescue.

Let’s imagine in this messaging system you can message your “followers”. You can also message followers of your followers. You can’t message anyone else. And that’s about all we know about this system. Oh, one more thing. We believe our system should not allow users to send messages to themselves. We’d like to check that somehow. Alloy here we come!

Let’s introduce this into Alloy with some basic entities:

sig User {
    follows: set User,
}

sig Message {
    sender: one User,
    recipient: one User
}

This defines two entities – User and Message. User has a set of users they follow. Message is defined as a 1-1 mapping between a sender and a receiver (two users). We do not care about the message content in formal verification.

Alright! Getting fun! We worked hard in our system. We know a thing or two about it. We have already made it impossible for one user to follow self. How do we express that in Alloy? With a fact. Facts are things that we claim are (or must be) true at all times.

fact NotFollowingSelf {
    all u: User |
    	u not in u.follows
}

Cool. Now let’s make this a little bit more interesting. We said our system limits messaging only to followers or followers of our followers.

fact MessageFollowersOrFoFs {
    all m: Message |
        (m.sender in m.recipient.follows)
        or 
        (some u: User |
	    u in m.recipient.follows and  
	    m.sender in u.follows)
}

Finally, let’s assert the big question – does our system prevent one to message themselves? This we won’t code as a fact. We will code it as an assertion. Meaning we actually want to check it. We don’t want to state it as a fact yet.

assert CannotMessageSelf {
    all m: Message |
        m.sender != m.recipient
}

check CannotMessageSelf

We save, execute and show the diagram. Looks like we found a counterexample! This is in other words a fault in our system. We found a bug! See diagram below.

Basically the bug happens because User0 and User1 follow each other. This is indicated by the bidirectional red arrows on the connecting line. With our current facts/rules, it is possible to send a message from User0 to User0 (self), due to mutual following. Now we can go back into our system engineering and fix this bug in some way!

After the bug is fixed in production, we can change the assertion to a fact. Then the Alloy’s reasoning about it updates. And that concludes this demo. I am just starting with Alloy and formal verification, and I find it quite interesting. Hope you enjoy it as well!