Alacrity is a domain-specific language for trustworthy decentralized applications. We use a cascading style of verification to help establish trust by users, by allowing an application's trusted code base to be very small, while enabling the application to be deployed in a wide variety of contexts. We will verify guarantees about program execution, compilation, correctness, security, and efficiency. It uses a suite of verification methods, like type theory, theorem proving, model checking, the strand spaces method, and dynamical system simulation.

This code is being developed as free software by LegiLogic, Inc., for the sake of Alacris, Ltd., that owns the copyright and publishes the code.

The Alacrity software is distributed under the GNU Lesser General Public License, version 2.1. See the file LICENSE.

You can watch on our github repository what we are currently working on.

As of June 2019, see notably the compiler we are writing in Haskell and the Rock, Papers, Scissors demo we are using as a benchmark application.

If you're using Emacs:

(add-to-list 'auto-mode-alist '("\\.mjs$" . javascript-mode))
(add-to-list 'auto-mode-alist '("\\.ala$" . javascript-mode))