Last week in the Distributed Systems Reading Group we read Aragog: Scalable Runtime Verification of Shardable Networked Systems. The paper describes an intriguing system from Microsoft Research and U Penn; it can analyze huge numbers of network events and find invariant violations that indicate bugs in the protocol. The invariants are expressed in a cute regular expression language, which Aragog parses and automatically decomposes into local and global verifier state machines. (But I don’t know why it’s called “Aragog”.)

Read Aleksey Charapko’s summary or watch my presentation.