Back to All Events

DCI Research presentation series: Jay McCarthy on 'Alacrity: A DSL for Simple, Formally-Verified DApps'

The Digital Currency Initiative hosts it’s weekly research presentation series. Invited speakers and DCI affiliates present on their projects and other relevant research.

Wednesday’s 3:00-4:00pm ET

Who: Jay Mc Carthy

Title: 'Alacrity: A DSL for Simple, Formally-Verified DApps‘

Abstract:

Alacrity is a domain-specific language for writing decentralized applications. It provides automatic solutions to a few key problems faced by blockchain developers: verifying that the DApp is trustworthy, ensuring the smart contract is consistent with client-side software, and abstracting over different blockchains.

Alacrity programs embed descriptions of properties about the behavior of the application: safety properties assert mistakes do not occur, and liveness properties assert desired outcomes do occur. The compiler automatically adds soundness properties that assert the application does not violate fundamental expectations of all DApps, such as that they conserve resources. The compiler automatically verifies correctness of these properties using the Z3 SMT theorem prover without intervention from programmers. This ensures that Alacrity programs are not susceptible to attacks that steal their resources, and ensures that untrusting participants can rely on the integrity and validity of the Alacrity program.

Alacrity programs incorporate the client-side behavior of participants, as well as on-chain behavior of the contract. The Alacrity compiler uses End-Point Projection to extract programs for each party and the contract, while guaranteeing each side makes the same assumptions about application state and communication protocols. This ensures that attacks do not exist that exploit the slightly different semantics of blockchain virtual machines and client-side programming languages.

Alacrity uses a blockchain-agnostic model of computation that allows programs to target different chains, including scaling solutions. This ensures that DApps can be designed independently of the deployment details and not be tied to the particular vagaries of any one platform.

The core philosophy of Alacrity is to design a highly constrained programming language that makes it easy to automatically prove the structural components of desirable properties about DApps, and makes it possible to easily prove the user-specific components of those properties. This is in contrast to designing an unconstrained language and providing a novel proving technique specialized for decentralized applications.

Invited guests only: If you are interested in joining the meeting in-person or remotely please contact Jacobsal@media.mit.edu