High-Assurance
Bitcoin Smart Contracts
Simplicity is a UTXO-based smart contracting language for Bitcoin, designed for verifiable security, financial correctness, and high-value applications.
Simplicity is a UTXO-based smart contracting language for Bitcoin, designed for verifiable security, financial correctness, and high-value applications.
A Simplicity contract is a spending condition on coins: it doesn't call other contracts, touch shared state, or loop without bound. That narrower model makes contracts easier to analyze. Their resource use is known ahead of time, and the language has a formal, machine-checked specification.
Execution costs bounded before you broadcast.
No external calls, so a smaller attack
surface.
A formally specified and verified core language, Rocq.
Only the executed branch is revealed on-chain.Simplicity complements Bitcoin Script with a low-level language that's expressive enough for advanced covenants and financial instruments while being formally verifiable for absolute predictability. Financial applications inherit a small, precisely defined base: bounded costs, no shared state, and no ambiguity in what the consensus layer will do. Developers write SimplicityHL, full nodes execute Simplicity. Learn more.
SimplicityHL looks like Rust: let, match, typed functions. Underneath, a program is a predicate over a transaction. It either authorizes a spend or it doesn't. There's no heap, no global state and no unbounded loops.
Everything a contract depends on is in front of you: the transaction it inspects, the witness data it receives, and the conditions it asserts. Nothing else can change that state while it runs.
The SimplicityHL compiler turns your code into Simplicity, the low-level language that full nodes execute. Common operations like hashing and signature checks run as optimized jets.
The EVM offers more flexibility and composability. Simplicity is deliberately more restrictive, trading some of that flexibility for stronger security guarantees.
Each contract keeps persistent storage that its functions read and write.
State lives in the coins (UTXOs) a contract locks and is carried forward in transaction outputs.
require(cond) reverts the call.
assert!(cond) fails the program, making the transaction invalid.
Gas is metered at runtime, and a reverted transaction still pays for the gas it used.
CPU and memory use have a static upper bound, known before broadcast. Invalid transactions are never mined.
msg.sender identifies the caller.
Signatures are checked explicitly, e.g. jet::bip_0340_verify.
Contracts call each other, and one call can trigger many others.
No contract calls. Several contracts compose by being spent in the same transaction.
Guarded against with checks-effects-interactions or ReentrancyGuard.
Not a class of bug. With no external calls, execution can’t be re-entered.
ERC-20 and ERC-721 contracts.
Native Liquid assets, issued at the protocol level. Contracts constrain how they move.
Each contract keeps persistent storage that its functions read and write.
State lives in the coins (UTXOs) a contract locks and is carried forward in transaction outputs.
require(cond) reverts the call.
assert!(cond) fails the program, making the transaction invalid.
Gas is metered at runtime, and a reverted transaction still pays for the gas it used.
CPU and memory use have a static upper bound, known before broadcast. Invalid transactions are never mined.
msg.sender identifies the caller.
Signatures are checked explicitly, e.g. jet::bip_0340_verify.
Contracts call each other, and one call can trigger many others.
No contract calls. Several contracts compose by being spent in the same transaction.
Guarded against with checks-effects-interactions or ReentrancyGuard.
Not a class of bug. With no external calls, execution can’t be re-entered.
ERC-20 and ERC-721 contracts.
Native Liquid assets, issued at the protocol level. Contracts constrain how they move.
Open-source protocols, demos, and research projects on Liquid.
Option and option-offer contracts, plus on-chain state management patterns, built with Smplx and tested on a local Liquid regtest.
A Simplicity-powered, decentralized price oracle for Liquid. The draft specification is public and development happens in the open.
A SHRINCS hash-based signature verifier written in Simplicity, used by the PQ Liquid Wallet to sign transactions on Liquid testnet.
Since Simplicity contracts are auditable and proveable before deployment, Simplicity offers unprecedented transparency and compliance assurance for financial institutions. Build programmable capital markets, issue assets, and settle trades—all on Bitcoin’s most secure sidechain, Liquid.
Open-source tools for writing, testing, and shipping SimplicityHL contracts.
The low-level language executed by full nodes, with a formal specification in Coq and reference implementations in C and Haskell.
The Rust-like high-level language and its compiler, simc, which compiles to Simplicity.
The standard library: overflow-checked arithmetic, 128- and 256-bit integers, secp256k1 helpers, and assertions.
A development framework for SimplicityHL: project CLI, Rust SDK, and a local Liquid regtest for integration tests.
Rust library for constructing, analyzing, and executing Simplicity programs.
Syntax highlighting, diagnostics, completion, hover, and go-to-definition for .simf files.
The language server behind the extension, usable from any LSP-capable editor.
A formatter for SimplicityHL code, also available as a library for editor and tool integrations.
Write, compile, and run SimplicityHL in the browser, with no local setup.
Start from the example contracts and the standard library, or write your own. Live on Liquid with native multi-asset support, and available on a Bitcoin signet for experimentation.
Deploy First Contract
Read Docs