Learn about Zen

F*—Formal Verification

All smart contract platforms have to deal with two problems: correct execution, and resource consumption. These are particularly hard to solve on a decentralized platform.

Zen takes F* as the starting point for defining smart contracts. F*, developed by Microsoft Research, is a functional language aimed at formal verification. Zen uses F*'s powerful proof techniques both to create proofs of correctness, and to prove that contracts execute in a limited amount of time. Proofs of correctness mean that anyone can write a new contract, implementing a particular kind of asset—a call option for example—and any user or contract can immediately discover and use that asset, with confidence that it performs as it claims to.

Bounded Computation

Proven resource bounds let miners accept and charge for any transaction which uses a contract, without suffering the risk of a denial of service attack. Proven resource bounds also enable a very significant optimization: contracts can be compiled to .NET bytecode at the moment they're created, making execution far faster than in an interpreted scripting language.

UTXOs & immutability

At the lowest level, Zen works similarly to Bitcoin, with transactions that unlock coins and lock them again to new outputs. This paradigm, often called the "unspent transaction output" or "UTXO" paradigm, means that every transaction, including a contract-generated transaction, has a clearly visible effect on the network consensus, even before running a contract or verifying transaction signatures. Zen contracts are immutable: once created, they never change internally. Contracts that need to store data do so on transaction outputs.

Active Contract Set & Offchain transactions

Zen contracts are paid to remain active for a set amount of time: after running out of payment, they become inactive, and no longer put a burden on miners or nodes. When reactivated, contracts appear with their exact original code, as if they never deactivated. This lets users trade contract-issued assets without using the contracts themselves, activating contracts only for final settlement.

The combination of the UTXO paradigm and the active contract set also allows for payment channels secured by a smart contract. Users can rapidly trade off-chain, swapping signed transactions which are only put onto the Zen network itself in the case of dispute, or to close a channel. Even very complex contracts can be held in reserve, never activated or paid for unless a dispute arises.

Oracles and External Data

Data from outside the Zen and Bitcoin blockchains enables agreements in Zen about events and assets from the external world. Zen oracles are efficient and well compensated: oracles use a merkle tree commitment to a large amount of data, and then can sell individual pieces of data, with proven payment for each piece.

Merged Consensus & Bitcoin Integration

In Zen miners mine the Zen blockchain, but are also required to monitor and validate the Bitcoin blockchain. Each block in Zen may refer to a number of bitcoin block headers, thus committing to the Bitcoin consensus.

Not only does this increase the number of Bitcoin nodes, it also makes Zen interoperable with Bitcoin. Any action on Bitcoin can affect events on Zen.

Zen contracts can monitor Bitcoin addresses, and automatically issue assets accordingly. But this means that Bitcoin users can take positions in Zen, enter contracts, and make secure decentralized deals, without leaving Bitcoin. A Zen contract that holds collateral enforces the appropriate payments in Bitcoin.


Bitcoin credits on Zen, secured by collateral, gain special properties. Contracts can understand the amount of collateral, the existence of actual bitcoins on the Bitcoin network, and the degree of risk resulting. They can then accept multiple different sources of Bitcoin credit, adjusting prices to match risk.