Analysis and verification of smart contracts with behavioural types

Smart contracts deployed on blockchain platforms are immutable once deployed, making correctness and security critical concerns that have led to substantial financial losses due to vulnerabilities. A significant proportion of these vulnerabilities stem from human-written code rather than blockchain infrastructure or cryptographic primitives. This observation motivates a paradigm shift from manual code development to model-driven approaches that generate semantically correct smart contracts from formal specifications. This thesis presents EDAM (Enhanced Data-Aware Machines), a behavioural model for specifying smart contracts that balances expressiveness with tractability. The framework extends traditional data-aware finite state machines [3] with essential features for a wide range of smart contract applications: dynamic role-based access control enabling runtime role assignment and revocation, participant management supporting unbounded and varying participants, and explicit modelling of inter-contract interactions through call tries with success and failure handling. The formal semantics of EDAM are grounded in established techniques from behavioural type theory, process calculi, and finite state machine theory, enabling rigorous reasoning about contract behaviour. The thesis contributes a comprehensive toolchain that integrates modelling, code genera- tion, test generation, and validation in a unified methodology. We develop a code generation engine that automatically produces Solidity smart contracts from EDAM specifications. The generated code faithfully implements the formal model, ensuring that the behaviour established at the model level is preserved in the executable code. The code generation process uses an intermediate JavaScript Object Notation (JSON) representation, which enables platform-agnostic code generation with ongoing extensions to support additional blockchain platforms such as Aptos. We present an automated test generation methodology that produces executable test suites from EDAM specifications. The approach combines symbolic trace generation using the formal semantics implemented in OCaml with randomized exploration of the Finite State Machine (FSM) network, enabling concrete trace derivation through random value assignment and Satisfiability Modulo Theories (SMT) constraint solving. This methodology systematically explores the state space to generate traces that exercise transitions, guards, and role constraints, producing executable test suites for standard testing frameworks such as Hardhat. The process is fully automated and can be integrated into the development workflow. Our evaluation demonstrates the expressiveness and practicality of the approach through a diverse benchmark of smart contracts, including contracts from the Azure repository [148], standard token contracts (Ethereum Request for Comments 20 (Token Standard) (ERC20)), Decentralized Finance (DeFi) protocols (Automated Market Makers (AMMs)), and multi- coordinator systems. The evaluation demonstrates expressiveness through the modelling of essential features, showing that the approach is able to model a wide range of smart contract features. The validation methodology employs a multi-faceted approach that combines code coverage analysis, mutation testing to validate the correctness of the generated code and the effectiveness of the test suites, and cross-validation by applying the generated tests to other established implementations. This cross-validation approach shows that our generated test suites are applicable to validate existing smart contract implementations, providing evidence of the quality and correctness of both the generated code and the testing methodology. The results empirically indicate that our model-driven approach produces contracts and test suites that preserve the structure and semantics of the formal model and can be applied to validate existing smart contract implementations. Unlike existing approaches that address isolated phases of the development lifecycle, EDAM provides an integrated toolchain that ensures consistency between specifications, vii generated code, and test suites. The framework shows that behavioural types provide a solid foundation for smart contract modelling and verification, enabling the development of unified frameworks that integrate modelling, code generation, test generation, and val- idation. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. The results show that model-driven approaches can produce high-quality smart contracts and comprehensive test suites, contributing to the advancement of secure smart contract development practices.