Validation of Automatically Synthesized Smart Contract Invariants: a validation framework for the FLAMES tool

Smart contracts are immutable programs deployed on blockchain platforms to enable decentralized applications and financial systems without intermediaries. However, their immutability and public execution make them especially vulnerable to security flaws, which can lead to irreversible significant financial losses. A promising approach to improve security is the use of invariants, properties that must always hold during contract execution. FLAMES (Fine-tuned Large Language Model for Invariant Synthesis) is a tool that leverages fine-tuned large language models to automatically generate security-relevant invariants for Solidity smart contracts. Automatically generating and validating such invariants remains a key challenge. This thesis evaluates FLAMES ability to synthesize and validate security-relevant invariants for Solidity smart contracts. The goal is to determine whether these invariants are both syntactically correct and semantically effective. To this end, two automated evaluation pipelines were implemented. The first tests whether smart contracts with injected invariants still compile successfully. The second examines whether these invariants prevent real exploits while preserving benign functionality. Experimental results show that FLAMES20K and FLAMES100K achieved high compilability rates and successfully patched known vulnerabilities. This work bridges the gap between theoretical invariant generation and practical smart contract security. By automating the validation of synthesized invariants, the proposed framework supports the development of more secure and reliable blockchain applications.