Skip to content
DSL for Secure DApps
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
ala Buttery, JS-like syntax Jun 28, 2019
archive Tweak simple auction contract Jul 12, 2019
docs Twitter link Jul 6, 2019
hs/alacrity While checkpoint Jul 17, 2019
js decode addresses into hex bytes, not bignums Jun 26, 2019
scripts/ethereum-devnet - Added a proper header type required by geth (but not necessary for … Jul 6, 2019
sol Add a solidity contract test Jun 24, 2019
z3 Fix strings in Z3 and make RPS ask for hands Jul 17, 2019
.gitignore Add Vim swap files to .gitignore Jun 18, 2019
.nojekyll Spell No Jekyll correctly Jun 24, 2019
LICENSE Draft pre-meeting Mar 19, 2019
Makefile Update Jul 5, 2019
index.html Rearranging Jun 28, 2019


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.

Being worked on

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.

Tips for Developers

If you're using Emacs:

(add-to-list 'auto-mode-alist '("\\.mjs$" . javascript-mode))
(add-to-list 'auto-mode-alist '("\\.ala$" . javascript-mode))
You can’t perform that action at this time.