- PhD Student
I am interested in formal specification of smart contracts (blockchain-based programs). Smart contracts are an ideal place for formal verification because (1) programs are small, (2) they often manage huge quantities of money, so the economic incentives align, (3) they are immutable after deployed, and (4) their specifications are interesting from various perspectives. My research focuses on the problem of ensuring a smart contract specification is faithful to its intended design.
I am thus tangentially interested in scalability/concurrency, automated market design, business models for the blockchain, etc. These topics can fall within the domain of specification formation in that if one is to build verified software to accomplish these tasks, one must be able to rigorously define desired properties. Often, desired properties are high-level and can thus be difficult to describe rigorously in a formal proof system.
