Building a Formally-Verified DApp with the Reach DSL, today!
Duration: 00:45:08
Speaker: Jay McCarthy
Type: Breakout
Expertise: Intermediate
Event: Devcon
Date: Jul 2026
In this hands-on workshop, we introduce Reach, take participants on a walkthrough of an example program, and guide them through implementing a basic DApp on their own. Reach, a new domain-specific language for decentralized applications, provides automatic solutions to the key problems faced by blockchain developers: ensuring the smart contract is consistent with client-side software, verifying the DApp is trustworthy, and abstracting over different blockchains. We then take a guided tutorial consisting of an example Reach program that implements a formally-verified two-party wager DApp. We explain the structure of the ~50 line Reach program and the structure of the ~50 line JavaScript frontend, and take a deep dive into properties that Reach formally guarantees. Participants will then work through a series of exercises implementing a different DApp with a similar structure to the sample program. They will leave with concrete experience using Alacrity that will enable them to build their own DApp. Prerequisites: Experience programming in JavaScript, have Docker installed on their machines to install the image of the Reach compiler and demo. It is recommended participants download and install this image before the workshop at: https://bit.ly/ReachIsTotallyAwesome. Experience with formal verification or stating DApp properties is NOT required.
