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 also use Balzac to design Bitcoin smart contracts [AB+18POST]. Some examples are given at the end of this tutorial.

Try our 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.


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

Smart contracts


  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: