“Reasoning About Knowledge in TLA+”

When we reason about a distributed protocol, we’re often talking about what each process knows at each point in time. “When the Raft leader gets an ack from one follower, it knows the log entry is majority-replicated.” “When the client gets a network error, it doesn’t know if it’s safe to retry the command.” These statements are examples of epistemic logic. But then, we usually specify the protocol with a temporal logic, like TLA+. TLA+ specs don’t express these knowledge properties: they’re just mindless state machines. Is there a way to reason about knowledge in TLA+?

A 1990 paper by Halpern and Moses, “Knowledge and Common Knowledge in a Distributed Environment”, describes epistemic logic for computer scientists. The math is beautiful, but is it useful? What if we could unify TLA+ (temporal logic) with epistemic logic?

I’ll present my research into mechanically verifying knowledge properties of TLA+ specifications. I.e., I can specify a property like, “the Raft leader doesn’t commit this operation until it knows it’s durable,” and automatically check if a TLA+ spec upholds this property. More complex properties are just as easy: “Eventually, agent 1 knows that agent 2 or agent 3 knows that everyone knows some fact.” I’ll show how epistemic logic connects to graph theory in order to verify such statements.

I’ve only recently begun exploring this topic, so I hope you’ll ask hard questions, share your own ideas, and help me decide on future research directions.

A. Jesse Jiryu Davis is a senior staff research engineer in the MongoDB Distributed Systems Research Group. He’s interested in distributed protocols, TLA+, formal specification, and testing that the code matches the spec. Jesse received his B.A. in computer science from Oberlin College in 2001. He joined MongoDB in 2011 as an engineer, and contributed to the Python, C, and C++ client libraries. He wrote some of the original specifications to which all MongoDB clients conform. He created Motor, the async Python driver for MongoDB. After serving for several years on the Replication and Serverless engineering teams, Jesse joined MongoDB Research in 2022.