In September 2025, I published a paper on my work towards a pure, formal specification of Bitcoin’s consensus rules.
Hornet Node and the Hornet DSL: A minimal, executable specification of Bitcoin consensus. T Sharp, September 2025. https://hornetnode.org/paper.html
I have now completed the C++ executable declarative specification for non-script block validation rules: 34 semantic invariants in total.
Background
Hornet is a minimal, executable specification of Bitcoin’s consensus rules, expressed both in declarative C++ and in a purpose-built domain-specific functional language.
It is implemented as a suite of modular, dependency-free, modern C++ libraries and includes a lightweight node capable of Initial Block Download (IBD).
Hornet’s concurrent, lock-free UTXO(1) engine achieves an 11× validation speedup over Bitcoin Core on full-chain replay (discussed in Bitcoin Optech Newsletter #391). All consensus logic is encapsulated by the declarative specification described below.
Update 2026-04-15
The question of whether a block is valid or invalid can – and should – be expressed as a Boolean, pure function without state changes or side effects.
Hornet aims to specify this logic declaratively and semantically, both in C++ and in a functional domain-specific language.
I have now completed the set of non-script block validation rules, organized with one semantic invariant per rule, with a total of 34 rules composed via a simple algebra. The first 15 rules are shown below.
// BLOCK VALIDITY SPECIFICATION
static constexpr auto kConsensusRules = All{
With{MakeHeaderContext, All{ // ## Header Rules
Rule{ValidatePreviousHash}, // A header MUST reference the hash of a valid parent block.
Rule{ValidateProofOfWork}, // A header's hash MUST achieve its own proof-of-work target.
Rule{ValidateDifficultyAdjustment}, // A header's proof-of-work target MUST satisfy the difficulty adjustment formula for the timechain.
Rule{ValidateMedianTimePast}, // A header timestamp MUST be strictly greater than the median of its 11 ancestors' timestamps.
Rule{ValidateTimestampCurrent}, // A header timestamp MUST be less than or equal to network-adjusted time plus 2 hours.
Rule{ValidateVersion} // A header's version number MUST NOT have been retired by any activated soft fork.
}},
With{MakeEnvironmentContext, All{ All{ // ## Local Rules
Rule{ValidateNonEmpty}, // A block MUST contain at least one transaction.
Rule{ValidateMerkleRoot}, // A block’s Merkle root field MUST equal the unique Merkle root of its transactions.
Rule{ValidateOriginalSizeLimit}, // A block’s serialized size excluding witness flags and data MUST NOT exceed 1,000,000 bytes.
Rule{ValidateCoinbase}, // A block's first transaction MUST be its only coinbase transaction.
Rule{ValidateSignatureOps}, // The total legacy signature-operation count over all input and output scripts MUST NOT exceed 20,000.
Each{TransactionsInBlock{}, All{
Rule{ValidateInputCount}, // A transaction MUST contain at least one input.
Rule{ValidateOutputCount}, // A transaction MUST contain at least one output.
Rule{ValidateTransactionSize}, // A transaction's serialized size excluding witness flags and data MUST NOT exceed 1,000,000 bytes.
Rule{ValidateOutputsNonNegative}, // All transaction output amounts MUST be non-negative.
...
The declarative specification separates what must be true from how it is computed. Each Rule line names a C++ function that validates the specific semantic rule in question, and also gives an English description of the rule being enforced.
The above statically-typed declarative graph is the executable specification of the semantic invariants that precisely determine consensus validity of a block in the Bitcoin network. Each Rule node names a validation function that returns a unique error code if and only if that property fails to hold.
We can parse the same code to automatically generate an English table of the semantic rules:
| ID | Rule |
|---|---|
| Header Rules | |
| H01 | A header MUST reference the hash of a valid parent block. |
| H02 | A header’s hash MUST achieve its own proof-of-work target. |
| H03 | A header’s proof-of-work target MUST satisfy the difficulty adjustment formula for the timechain. |
| H04 | A header timestamp MUST be strictly greater than the median of its 11 ancestors’ timestamps. |
| H05 | A header timestamp MUST be less than or equal to network-adjusted time plus 2 hours. |
| H06 | A header’s version number MUST NOT have been retired by any activated soft fork. |
| Local Rules | |
| L01 | A block MUST contain at least one transaction. |
| L02 | A block’s Merkle root field MUST equal the unique Merkle root of its transactions. |
| L03 | A block’s serialized size excluding witness flags and data MUST NOT exceed 1,000,000 bytes. |
| L04 | A block’s first transaction MUST be its only coinbase transaction. |
| L05 | The total legacy signature-operation count over all input and output scripts MUST NOT exceed 20,000. |
| L06 | A transaction MUST contain at least one input. |
| L07 | A transaction MUST contain at least one output. |
| L08 | A transaction’s serialized size excluding witness flags and data MUST NOT exceed 1,000,000 bytes. |
| L09 | All transaction output amounts MUST be non-negative. |
| … |
For the full declarative C++ spec, see hornet/src/hornetlib/consensus/rules/spec.h at main · tobysharp/hornet · GitHub
For the resulting semantic summary table, see https://hornetnode.org/spec.html.
To read more about Hornet and how it relates to other projects, see https://hornetnode.org/overview.html.
Future work
The spending rule S06: “A non-coinbase input MUST satisfy the spent output’s locking script” is correct, but on its own clearly doesn’t capture the internal complexity of script execution. I am working towards a separate layer of specification for script rules.
The declarative C++ specification is a step towards a pure, functional domain-specific language for a Bitcoin consensus spec. This will be implemented in a future iteration, together with an interpreter and/or compiler. Here is an example of the Hornet DSL:
// The total number of signature operations in a block MUST NOT exceed the consensus maximum.
Rule SigOpLimit(block ∈ Block)
Let SigOpCost : (op ∈ OpCode) -> int32
|-> ⎧ 1 if op ∈ {Op_CheckSig, Op_CheckSigVerify },
⎨ 20 if op ∈ {Op_CheckMultiSig, Op_CheckMultiSigVerify},
⎩ 0 otherwise
Require Σ SigOpCost(inst.opcode)
∀ inst ∈ script.instructions
∀ script ∈ tx.inputs.scriptSig ⧺ tx.outputs.scriptPubKey
∀ tx ∈ block.transactions
≤ 20,000
Conclusion
I welcome feedback from the developer community. In particular, do you believe there is value in a formal specification of consensus rules? Are there any aspects of Hornet that you like or dislike? Are there any rules that you believe are missing, redundant, unclear, or incorrect? I also welcome any bug reports. Thank you.