A distributed systems compiler, providing compilation from abstract model-checkable Modular PlusCal specifications into Go.

Have a look at our demo projects, such as a Raft-based key-value store, a CRDT implementation, and a primary-backup key-value store. The codebase also includes a variety of utilities for linking abstract specification concepts with concrete implementations. Commonly used examples are TCP connections, failure detectors, filesystem access, and native Go channels.

My MMath thesis work. Designed to make Interface Definition Language implementation easier, it's an impure functional language with fully out-of-order processing, making order-of-operations bugs, even involving pointers, impossible.

mel is a declarative, rule-based Model Extraction Language for extracting facts from XML-structured models of software.

This is a collaboration with WatForm, centered around Rob Hackman's thesis under Joanne M. Atley. I contributed evaluation work, comparing mel with XQuery, a web standard with related features.