Smart Contract Validation based on Linear Types

July 27, 2026

Most blockchain-based decentralized applications heavily rely on the correctness and security of smart contracts to ensure secure asset management and the execution of transactions. Smart contracts deal with various kinds of digital resources, including cryptocurrencies, NFTs, and access permissions, which need precise tracking and validation to avoid vulnerabilities such as unauthorized duplication or misuse. Given the immutability of the blockchain, ensuring correctness at deployment time is crucial, since postdeployment fixes are impossible. Current techniques including fuzzing, symbolic execution and formal verification cannot detect some of these bugs and resource validation requirements, leading to financial losses. This thesis proposes an approach to smart contract validation through a type system that enforces resource constraints based on linear types. To demonstrate this approach, we developed an experimental smart contract language that enables programmers to define high-level quantitative types and perform operations on resources that are sound both logically and operationally. This framework addresses critical challenges in blockchain systems, including the double-spending problem, while offering a foundation for integrating these principles into real-world languages like Solidity or Move. By enhancing smart contract validation, our work contributes to the broader adoption of blockchain towards a more secure and trusted platform for financial, legal, and operational purposes.

Authors in the community:

• 

  R

  Renato Tito Antunes de Meireles Martins

  ist1102314

Supervisors of this institution:

• 

  L

  Luís Caires

  ist414516

electrical-engineering-electronic-engineering-information-engineering - Electrical engineering, electronic engineering, information engineering

eng - English

Instituto Superior Técnico