Consolidating Smart Contracts with Behavioral Contracts

Explore a 19-minute conference talk from PLDI 2024 that introduces ConSol, a Solidity language extension supporting behavioral contracts for smart contract development. Delve into the design and implementation of ConSol, which provides a modular specification and monitoring system for both functional and latent address behaviors in smart contracts. Learn how ConSol allows programmers to attach specifications to first-class addresses and monitor violations during address invocation. Discover the effectiveness of ConSol in expressing critical conditions and preventing attacks through an evaluation of 20 real-world cases. Examine the efficiency of ConSol and its impact on gas consumption compared to manually inserted assertions. Gain insights into how behavioral contracts can enhance the robustness and readability of smart contract code by separating specifications from implementations.