Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem

We are pleased to announce that Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts. The grant is part of its recently launched 250 Million ALGO Ecosystem Grants Program, a multi-year program that aims to support research and development of the Algorand ecosystem. We are very excited to have the opportunity to collaborate with Algorand in forming the future of Algorand’s smart contract architecture and supporting its growing community of developers. We have previously successfully completed a prior engagement with Algorand to formally model and verify safety of the platform’s consensus protocol, and we look forward to using the knowledge and experiences gained in this new engagement.

Through this new engagement with Algorand, our goal is to develop a framework for Algorand’s advanced architecture of smart contracts using the K framework. The framework will facilitate a formal semantic approach to smart contract development, implementation, testing and verification. This will help lay the foundation for developing correct-by-construction smart contract tools that empower smart contract developers to build secure and reliable applications over the Algorand platform. It also sets the stage for further advancements to the architecture in the future.

At the heart of this framework is a formal definition in K of Algorand’s smart contract language, an adaptation of Blockstack Clarity language, and its interface with the blockchain. The formalization will also include Algorand’s transaction logic and the semantics of Algorand’s on-chain Transaction Execution Approval Language (TEAL). The framework enables mathematically well-founded and unambiguous definitions that can be used to automatically generate a wide variety of tools, including executable documentation of the system, language interpreters and efficient reference implementations for running and debugging programs, model-based testing and semantic coverage tools, static analysis tools, symbolic execution engines and reachability analysis and model checking tools.

We at Runtime Verification pioneered this K semantics-based approach and have plenty of academic and commercial experience in applying it to language design, implementation and verification, especially in the blockchain space. In addition to providing K-based formal modeling and verification services, we are transforming some of these services into products that the community can use, such as Firefly, a formal system for defining high-assurance smart contracts in Ethereum. We see this engagement as the first step towards developing such a product for the Algorand platform.