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.
```cpp
// 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 https://github.com/tobysharp/hornet/tree/main/src/hornetlib/consensus/rules/spec.h
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.
T#
--
You received this message because you are subscribed to the Google Groups "Bitcoin Development Mailing List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to bitcoindev+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n%40googlegroups.com.