Projects

Distributed systems are difficult to design and implement correctly. In response, both research and industry are exploring applications of formal methods to distributed systems. A key challenge in this domain is the missing link between the formal design of a system and its implementation. Today, practitioners bridge this link through manual effort.

We present a language called Modular PlusCal that extends PlusCal by cleanly separating the model of a system from a model of its environment. We then present a compiler tool-chain called PGo that automatically translates MPCal models to TLA+ for model checking, and that also compiles MPCal models to runnable Go code. PGo provides system designers with a new ability to model and check their designs, and then re-use their modeling efforts to mechanically extract runnable implementations of their designs.

In 2021, I started the Peydaa project. Peydaa is a non-profit platform to make transparency in the Iranian job market. It is a website where people can anonymously share their salary and experience of working in companies with others. So far, more than 1000 users have shared their salaries and experiences on Peydaa.

Verify the communication of your microservices by writing contracts for your RPCs. gRPC Go Contracts provides contract programming (aka Design by Contract) for gRPC methods written in Go and supports preconditions and postconditions. In the case of contract violation, it logs the contract error message and its parameters.