The aim of Juvix is to help write safer smart contracts. Juvix implements many desirable features for a smart contract programming language.

The Juvix team created the project Witch. Witch combines different proof strategies to enable users to profit from proof assistants without an in-depth understanding of the theory behind it

Juvix is designed as a smart contract verification and execution language, where efficient compilation is key, as otherwise any inefficient compilation to the primitives of a virtual machine on a decentralised blockchain will result in extra funds spent in order to execute any given program.

This post enumerates the various theoretical ingredients in Juvix that we think will enable it to meet these challenges, describes the current state of specification and implementation.

Juvix is designed to address the problems that we have experienced while trying to write & deploy decentralised applications.

Here at Cryptium Labs, besides delegation services and protocol development, we are also developing a smart contract language called Juvix. A few talks I went to at Devcon 5 have me reflecting on some thoughts of smart language design.

F* is a dependently typed language based off of Hoare Type Theory, refinement types, a SMT solver and features an effect system. All these features culminate in a high level language that excels at verifying and generating low level code.