Bitcoin Abstract Language, analyZer and Compiler

BALZaC is an high-level language for writing transactions, verifying their correctness, and compiling them into actual Bitcoin transactions. It is based on the formal model proposed in [AB+18FC].

You can install the IDE as a Eclipse plugin, or try the web editor.

The project is open source, and you are welcome to contribute to our repository.

BALZaC is developed by the Blockchain@Unica group of the University of Cagliari.


Installation and Configuration

Smart contracts


BALZaC is intended for research purposes only. Do not use it to create mainnet transactions, or do it at your own risk.


  1. Atzei, M. Bartoletti, S. Lande, R. Zunino. A formal model of Bitcoin transactions. In Financial Cryptography and Data Security, 2018. Preprint:
  1. Atzei, M. Bartoletti, T. Cimoli, S. Lande, R. Zunino. SoK: unraveling Bitcoin smart contracts. In Principles of Security and Trust (POST), 2018. Preprint: