The Jus Programming Language: Towards A Functional Language For Secure and Verifiable Smart Contracts On Tezos

The development of secure and verifiable smart contracts remains a critical challenge in blockchain technology. This paper introduces Jus, a functional language designed to address these challenges on the Tezos platform. Jus combines functional programming principles, such as immutability and purity, with domain-specific constructs tailored for smart contracts, including explicit state-transition systems and advanced type-theoretic features. A prototype interpreter for Jus has been implemented, enabling the execution of simple contracts and validating the language’s core design principles. Preliminary results demonstrate Jus’ potential to simplify contract development, enhance security, and facilitate formal verification. By aligning with Michelson, Jus aims to provide an efficient and expressive environment for developing robust decentralized applications. Future work will focus on extending the interpreter and developing a compiler to translate Jus contracts into Michelson bytecode, paving the way for broader adoption within the Tezos ecosystem.