The Jus programming language : towards a functional language for secure and verifiable smart contracts on Tezos

O desenvolvimento de smart contracts ainda enfrenta desafios significativos, especialmente no que diz respeito à segurança, previsibilidade de execução e capacidade de verificação formal. Erros de implementação podem causar perdas irreversíveis, e muitas linguagens existentes não oferecem mecanismos adequados para garantir propriedades críticas antes da implantação. Diante desse cenário, esta dissertação propõe Jus, uma linguagem de domínio específico, funcional e orientada à verificação, projetada para facilitar a construção de contratos inteligentes mais seguros e verificáveis na blockchain Tezos. Jus combina princípios de programação funcional (como pureza, mutabilidade e tipagem estática) com uma arquitetura inspirada em autômatos, na qual cada contrato é representado como um sistema explícito de transição de estados. Esse modelo torna o comportamento do contrato mais revisível e favorece análises formais. A linguagem também inclui construções específicas do domínio, como tipos monetários, operações de escrow, mecanismos de multiassinatura e gatilhos temporais, que ajudam a expressar adrões recorrentes de forma segura. Para avaliar a proposta, foi desenvolvido um interpretador protótipo, utilizando ANTLR na análise sintática, além de dois estudos de caso representativos. Esses estudos demonstram que Jus ermite expressar contratos reais de maneira declarativa, sem estado mutável e com comportamento estruturado, facilitando a verificação estática de invariantes. A dissertação também apresenta uma estratégia conceitual de ompilação para Michelson (a linguagem nativa do Tezos) com ênfase na preservação semântica e na preparação para ferramentas de verificação existentes no ecossistema. Por fim, é proposto um roteiro de formalização que inclui embedding do sistema de tipos em provadores, mecanização da semântica operacional, model checking do sistema de transições e o desenvolvimento futuro de um compilador verificado. Os resultados mostram que Jus epresenta um passo em direção a smart contracts mais auditáveis, seguros e adequados a contextos de alto valor na blockchain Tezos.

Smart contract development still faces major challenges in terms of security, predictability, and formal verification. Implementation errors can lead to irreversible losses, and many existing languages offer limited support for expressing or proving critical correctness properties prior to deployment. To address these limitations, this dissertation proposes Jus, a functional, verification-oriented domain-specific language designed to support the development of secure and formally analyzable smart contracts on the Tezos blockchain. Jus integrates functional programming principles (purity, immutability, and static typing) with an automata-based architecture in which each contract is modeled as an explicit state-transition system. This structure improves predictability and supports rigorous reasoning about contract behavior. The language also provides domain-specific constructs, such as monetary types, escrow operations, multisignature workflows, and time-based triggers, enabling developers to express common blockchain patterns safely and concisely. To evaluate the language, a prototype interpreter was implemented using ANTLR for parsing, along with two representative case studies. These case studies demonstrate that Jus enables the declarative and mutation-free expression of real smart contracts, helping capture invariants at compile time and facilitating formal analysis. The dissertation further outlines a conceptual compilation strategy targeting Michelson (the low-level language of Tezos), highlighting semantic preservation, resource analysis, and compatibility with existing verification tools. Finally, the work proposes a roadmap for the formalization of Jus, including type-system embedding in proof assistants, mechanization of the operational semantics, model checking of transition systems, and the future development of a verified compiler. The results indicate that Jus is a promising step toward more secure, auditable, and formally verifiable smart contracts on the Tezos blockchain.