Juvix is a research programming language created by
Heliax as a first step toward creating more
robust and reliable alternatives for formally verified smart contracts
than existing languages. The Juvix language is constantly evolving,
open-source, functional, and statically typed with special support for
predicates to the
language, which can be deployed to various distributed ledgers including
The Juvix language and related tools are documented in the Juvix
book. To write and test Juvix programs,
you can use your favorite text editor and the
juvix command line tool.
However, we recommend using the
Emacs or the plugin in
The following links are clickable versions of their corresponding Juvix
programs. The HTML output is generated by running
juvix html --recursive FileName.juvix.
The Juvix standard library contains common functions that can be used in Juvix programs.
The easiest way to install Juvix on MacOS is by using Homebrew.
To install the homebrew-juvix tap, run:
brew tap anoma/juvix
To install Juvix, run:
brew install juvix
Helpful information on the shell can also be obtained by running:
brew info juvix
A binary executable is available on the Juvix release page.
git clone --recursive https://github.com/anoma/juvix.git cd juvix stack install
On MacOS you can alternatively run the following command for Homebrew.
--HEAD used below is optional, use it to build the latest
version of Juvix in the
main branch on Github.
brew install --build-from-source --HEAD juvix --verbose
After installation run
juvix --help to see the list of commands
available. See CLI usage
for descriptions of common tasks.
Run Juvix doctor to check your system setup:
This is the Juvix source code of the traditional Hello World program.
-- HelloWorld.juvix module HelloWorld; open import Stdlib.Prelude; main : IO; main := putStrLn "hello world!"; end;
To compile and run a binary generated by Juvix, save the source code to
a file called
HelloWorld.juvix and run the following command from the
directory containing it:
juvix compile HelloWorld.juvix ./HelloWorld
You should see the output:
The source code can also be compiled to a WebAssembly binary. This
requires some additional setup. See Installing
in the documentation for more information. You can also run
juvix doctor to check your setup.
juvix compile --target wasm HelloWorld.juvix wasmer HelloWorld.wasm
Juvix allows us to write programs with a high degree of assurance. The Juvix compiler runs several static analyses during the compilation phase to guarantee no runtime errors. Analyses permormed during this phase include scope, termination, arity, and type checkiqng. As a result, functional programs, especially validity predicates, can be written with greater confidence that they will be free of runtime errors.
Some of the language features in Juvix include:
- unicode syntax
- parametric polymorphism
- inductive and parametric data types
- higher-order functions
- implicit arguments
- holes in expressions
- axioms for non-computable terms
Additionally, the foreign and compile blocks syntax enable developers to
compile a program to different backends including the
C language. The
Juvix module system further permits splitting programs into several
modules to build libraries which can be later documented by generating
HTML files based on the codebase, see for example, the Juvix standard
library's website. For futher
details, please refer to the Juvix
book which includes our latest
For the language:
- lambda expressions
- tail call optimization
- inference for mutually recursive functions
- compilation to circuits
- coverage checking (i.e. exhaustiveness and useless clauses)
For the compiler:
- Init command
- Better documentation tool:
juvix doc MyFile.juvix
We would love to hear what you think of Juvix! Join us on the Anoma Discord.