BALZaC

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.

Warning

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

Getting Started

• Balzac in a nutshell
• Transaction signatures
• Raw Transactions
• Assertions

Language Specification

• Transactions
  • Inputs
  • Outputs
  • AbsLock
  • RelLock
• Expressions
  • Literals
  • Boolean operations
  • Arithmetic operations
  • String Concatenation
  • BTC
  • References
  • Conditional
  • Numerical Expressions
  • Hash functions
  • Key Operations
  • Cryptographic functions
  • Time constraints
  • Transaction operations
  • Placeholders
• Types
• Editor syntax
  • Package
  • Comments
  • Network
  • Constants
  • Transactions
  • Evaluation

Smart contracts

• Oracle
• Escrow
• Timed Commitment

References

[AB+18FC]

14. Atzei, M. Bartoletti, S. Lande, R. Zunino. A formal model of Bitcoin transactions. In Financial Cryptography and Data Security, 2018. Preprint: https://eprint.iacr.org/2017/1124.pdf

[AB+18POST]

14. Atzei, M. Bartoletti, T. Cimoli, S. Lande, R. Zunino. SoK: unraveling Bitcoin smart contracts. In Principles of Security and Trust (POST), 2018. Preprint: https://eprint.iacr.org/2018/192.pdf