Hornet Update: A declarative executable specification of Bitcoin consensus rules

[Toby Sharp]

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#

[er...@voskuil.org]

Hi Toby,

I very much support your effort to produce a formal specification. Libbitcoin requires the isolation of consensus rules into purely functional boolean methods with names that identify the rule under evaluation. I've pasted the list of these header/tx/block functions below. You'll notice that `interpreter::connect()` is evaluated with `transaction::connect()`. This declarative pattern continues into all of script evaluation, but is too large to include. The declarative opcode evaluation portion can be seen here: https://github.com/libbitcoin/libbitcoin-system/blob/master/include/bitcoin/system/impl/machine/interpreter.ipp . There are of course certain design decisions that affect the specific organization, but the outcome is the same. Each rule requires and name and functional, isolated evaluation.

We see this as the way forward, and are excited to see you tackling the formality aspect. We are looking forward to collaborating with you on it. It is essential to the usefulness of the formalization that it be applied to a node in widespread use. So while we long ago implemented the required consensus isolation, we have spent years on the many other aspects of high-performance node design. This gives me hope that we can make meaningful progress on the formalization as well. As you know there is real interest in the community to make this happen.

Best,
Eric

// header
// ----------------------------------------------------------------------------

code header::check() const
{
if (is_invalid_proof_of_work())
return error::invalid_proof_of_work;
if (is_futuristic_timestamp())
return error::futuristic_timestamp;

return error::block_success;
}

code header::accept(const context& ctx) const
{
if (ctx.is_insufficient_version(version_))
return error::insufficient_block_version;
if (ctx.is_anachronistic_timestamp(timestamp_))
return error::anachronistic_timestamp;
if (ctx.is_invalid_work(bits_))
return error::incorrect_proof_of_work;

return error::block_success;
}

// transaction
// ----------------------------------------------------------------------------

code transaction::check() const
{
const auto coinbase = is_coinbase();

if (is_empty())
return error::empty_transaction;
if (coinbase && is_invalid_coinbase_size())
return error::invalid_coinbase_script_size;
if (!coinbase && is_null_non_coinbase())
return error::previous_output_null;

return error::transaction_success;
}

code transaction::check(const context& ctx) const
{
const auto bip113 = ctx.is_enabled(bip113_rule);

if (is_absolute_locked(ctx.height, ctx.timestamp,
ctx.median_time_past, bip113))
return error::absolute_time_locked;

return error::transaction_success;
}

code transaction::accept(const context&) const
{
if (is_coinbase())
return error::transaction_success;
if (is_missing_prevouts())
return error::missing_previous_output;
if (is_overspent())
return error::spend_exceeds_value;

return error::transaction_success;
}

code transaction::confirm(const context& ctx) const
{
const auto bip68 = ctx.is_enabled(bip68_rule);

if (is_coinbase())
return error::transaction_success;
if (bip68 && is_relative_locked(ctx.height, ctx.median_time_past))
return error::relative_time_locked;
if (is_immature(ctx.height))
return error::coinbase_maturity;
if (is_unconfirmed_spend(ctx.height))
return error::unconfirmed_spend;
if (is_confirmed_double_spend(ctx.height))
return error::confirmed_double_spend;

return error::transaction_success;
}

code transaction::connect(const context& ctx) const
{
if (is_coinbase())
return error::transaction_success;

for (auto in = inputs_->begin(); in != inputs_->end(); ++in)
if (const auto ec = interpreter::connect(ctx, *this, in))
return ec;

return error::transaction_success;
}

// block
// ----------------------------------------------------------------------------

code block::check() const
{
if (is_oversized())
return error::block_size_limit;
if (is_first_non_coinbase())
return error::first_not_coinbase;
if (is_extra_coinbases())
return error::extra_coinbases;
if (is_forward_reference())
return error::forward_reference;
if (is_internal_double_spend())
return error::block_internal_double_spend;
if (is_invalid_merkle_root())
return error::invalid_transaction_commitment;

return check_transactions();
}

code block::check(const context& ctx) const
{
const auto bip141 = ctx.is_enabled(bip141_rule);
const auto bip34 = ctx.is_enabled(bip34_rule);
const auto bip50 = ctx.is_enabled(bip50_rule);

if (bip141 && is_overweight())
return error::block_weight_limit;
if (bip34 && is_invalid_coinbase_script(ctx.height))
return error::coinbase_height_mismatch;
if (bip50 && is_hash_limit_exceeded())
return error::temporary_hash_limit;
if (bip141 && is_invalid_witness_commitment())
return error::invalid_witness_commitment;

return check_transactions(ctx);
}

code block::accept(const context& ctx) const
{
const auto bip16 = ctx.is_enabled(bip16_rule);
const auto bip42 = ctx.is_enabled(bip42_rule);
const auto bip141 = ctx.is_enabled(bip141_rule);

if (is_overspent(ctx.height, bip42))
return error::coinbase_value_limit;
if (is_signature_operations_limited(bip16, bip141))
return error::block_sigop_limit;

return accept_transactions(ctx);

[Toby Sharp]

Hi Eric,

Thanks for your thoughtful and encouraging comments, and for sharing some of the libbitcoin implementation.

I find libbitcoin to be impressive in scope and pleasant in design, and hope that it continues to gain recognition and adoption. I also find it significant that Hornet and libbitcoin independently converged on a principle of isolated consensus rules, and soon it will be interesting to compare them side-by-side and study any differences.

For this reason, I think it's rather good that the Hornet spec and code has been developed independently from libbitcoin, since two independent and convergent derivations greatly strengthen the case that the resulting rule set is complete and correct -- not an artifact of a single codebase's design assumptions.

The architectural distinction I'd note is in composition. Libbitcoin isolates rules as predicates but composes them inside phase-specific methods as if-chains. This is excellent for a clean and readable node implementation. Hornet goes further and composes them in a static declarative graph using an algebra of combinators (All, With, Each). This makes the spec itself a first-class data structure that is traversable, renderable, executable, and later replaceable with a DSL representation. I see this as the step that takes consensus isolation toward language-neutral consensus specification.

On widespread use: Hornet Node today is more of an experimental client for validation and IBD than a fully functional node. This is by design, as the main target at this stage is the neutral specification, and demonstration of how it can be efficiently and verifiably implemented for IBD. Collaboration with existing clients would be ideal.

Some suggestions on collaboration might include: cross-validating libbitcoin's predicate set against Hornet's 34 semantic invariants to identify and resolve any divergence; joint review of the DSL as it develops; discussion on how we might verify that libbitcoin exactly implements the specification; and sharing a corpus of edge-case test vectors.

Happy to take any of this to direct email.

Best wishes,
T#



Sent with Proton Mail secure email.