Verificação Formal e Sugestão Automática de Propriedades em Contratos Inteligentes: Integrando LLMs e Preservação Semântica

Descrição

Contratos inteligentes são programas autônomos executados em plataformas blockchain, cuja corretude e segurança são cruciais para garantir a inte aplicações descentralizadas. Este trabalho propõe o uso de técnicas de verificação formal como uma abordagem sistemática para assegurar a preser\ em transformações aplicadas a contratos inteligentes, incluindo refatorações, otimizações e traduções entre linguagens. Além disso, exploramos o us linguagem de grande porte (LLMs) como ferramenta auxiliar para sugerir propriedades de segurança e comportamento esperados dos contratos, e pr formais para verificar a correção dessas sugestões. A abordagem visa combinar o poder expressivo das LLMs com a robustez das provas formais, pro confiança no desenvolvimento e evolução de contratos inteligentes.