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.

[er...@voskuil.org]

Hi Toby,

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

Of course, you as well.

> 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).

I wouldn't call this an architectural distinction given that it can be implemented over the set of rules in a matter of minutes. The design challenge is in properly identifying and functionally isolating each rule. The block/header/tx rules are the low hanging fruit. We implemented this well over 10 years ago, so I also don't know if I would consider it convergent:

https://github.com/libbitcoin/libbitcoin-system/commit/4c6cd2874f5e0b490dc1d7c020ace52858fb1b84#diff-d80e987b7f0628275c6e7318733e70848645f499b8a33c08f66d0f65b3f64e77R399

There are maybe two orders of magnitude more work in script evaluation alone (link to one part of it previously posted). And then there is at least deserialization, storage, and chain organization - all while making this fit architecturally into performance and public interface constraints. Providing meaningful formal verification across that space is a monumental task, which is why I'm encouraged that you are taking it on. But it does seem to me that you may be underestimating it, even within Hornet's limited design target.

> 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

This work can eventually produce a specification. The problem however will remain faith in the correctness of the specification itself. Verification cannot reasonably be applied to existing bitcoind implementations (and there are a lot of them both in versions and in forks), and modifying them to the point where this is feasible becomes a new architecture (which is what we have done). My prior comment on "widespread use" is about this specific problem. To solve this requires two things:

(1) at least one fully consensus-verifiable node implementation.
(2) the verified implementation(s) are predominant in economic use.

Once this is the case, the rules become useful in the verification of other implementations.

> 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.

This all sounds reasonable. However, for us to invest limited resources it requires that the outcome be meaningful. This small subset of the problem could provide a proof of concept, which we could use to measure scope across the entire surface. At that point we could balance further work on (1) above against also achieving (2).

>> Are there any rules that you believe are missing

From my reading of rule names and descriptions here:

https://github.com/tobysharp/hornet/blob/main/src/hornetlib/consensus/rules/rules.h

It appears that Hornet is missing the rule prohibiting forward references within a block.

https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block.cpp#L397-L417

This is a partial ordering constraint (is_forward_reference) that's easy to miss because it's just a bitcoind implementation artifact. By isolating this behavior to its own rule, not only does it not get missed, but rule evaluation also becomes order independent and therefore parallelizable.

Otherwise there are potential malleation issues to deal with depending on how blocks/headers are being managed. This can affect consensus behavior (via archival) while not showing up as an issue in these rules. There is also the rule prohibiting double spends, which can invalidate a context-free block (is_internal_double_spend), which would otherwise not be caught until contextual checks (so is more of an optimization and malleation guard).

https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block.cpp#L422-L434

We avoid applying redundant rules except in the case of unconfirmed tx validation, as it becomes necessary for DoS protection. But we label these as "guards" not "rules". In this case the rules are block-level but must be evaluated when accepting unconfirmed txs. The above is_internal_double_spend rule is a bit of an exception but it's context free, legitimately detects invalidity, precludes a type of malleation, and short-circuits a later more comprehensive/costly check.

Best,
Eric

[Toby Sharp]

> It appears that Hornet is missing the rule prohibiting forward references within a block.

This is implied by Rule S02: "A transaction input MUST reference a previous transaction output that remains unspent." However, to make it clearer, I will rewrite it as:

"S02: A transaction input MUST reference a preceding transaction output that remains unspent."

> Otherwise there are potential malleation issues to deal with depending on how blocks/headers are being managed. This can affect consensus behavior (via archival) while not showing up as an issue in these rules.

That would be an implementation correctness detail rather than part of a declarative spec.

The intention here is to specify what must be true for consensus validity rather than how it should be computed.

Best wishes,
T#

[er...@voskuil.org]

> > It appears that Hornet is missing the rule prohibiting forward references
> within a block.
>
> This is implied by Rule S02: "A transaction input MUST reference a previous
> transaction output that remains unspent." However, to make it clearer, I will
> rewrite it as:
>
> "S02: A transaction input MUST reference a preceding transaction output that
> remains unspent."

As I understand it, the rule in question:

// Returns success if every spending input in this block references an existing unspent output.
consensus::Result QueryPrevoutsUnspent(const protocol::Block& block) const override {
Assert(&block == joiner_->GetBlock().get());
if (!joiner_->WaitForQuery()) return consensus::Error::Spending_PrevoutNotUnspent;
return {};
}

can only fail if the query fails, and the query itself is not subject to verification. In this case the consensus rule is implemented as a side effect of the query (as it is in bitcoind), and the query itself is not subject to verification. I would consider this a missing rule from the perspective of verification. It is true that the store must provide fidelity in any case (what goes in must come out). That alone presents significant issues for verification. But at least it's straightforward to define. But in this case the query is not just returning outputs that have been stored in the block total ordering.

The query is constructing a temporary map, accumulating block-internal spends into that map in a specific order, populating the results, and effectively enforcing the forward reference constraint as side effect of the population implementation. These outputs are not placed into the utxo store until after the block is validated. In other words, the consensus rule is evaluated entirely within the scope of the query; it is not a consequence of simple store fidelity, and is not a consequence of a verified rule. It's lurking in an unverified query. If another implementation was to populate prevouts differently (e.g., in parallel), and with full fidelity, the ordering constraint easily disappears and is not caught by verification. This has happened, and IIRC resulted in the loss of a block by a miner. This is the type of consensus break that verification presumes to preclude.

> > Otherwise there are potential malleation issues to deal with depending on
> how blocks/headers are being managed. This can affect consensus behavior
> (via archival) while not showing up as an issue in these rules.
>
> That would be an implementation correctness detail rather than part of a
> declarative spec.
>
> The intention here is to specify what must be true for consensus validity rather
> than how it should be computed.

The whole point is verifying implementation correctness. Calling it out of scope doesn't really solve the problem. Merkle root malleation has resulted in consensus failure (bitcoin core). Transaction deserialization has resulted in consensus failure (btcd). Store infidelity has resulted in consensus failure (bitcoind). Cryptographic library bugs have produced consensus bugs that were preemptively patched (openssl). These types of issues are more common in modern history than what one might consider "rules". The so-called rules are actually much easier to deal with.

Airing out some of these real difficulties has been worthwhile. In my experience people have an overly optimistic view of what can be achieved by both formal verification and the attempt to create a shared script implementation. I'm hopeful, but I also try to stay grounded. I'll give further responses offline.

Best,
Eric

https://nvd.nist.gov/vuln/detail/CVE-2022-39389
https://nvd.nist.gov/vuln/detail/CVE-2012-2459
https://nvd.nist.gov/vuln/detail/CVE-2013-3220