# Hornet Update: A declarative executable specification of consensus rules

**URL:** <https://delvingbitcoin.org/t/hornet-update-a-declarative-executable-specification-of-consensus-rules/2420>\
**Category:** Implementation\
**Created:** [April 15, 2026, 10:46pm UTC](https://delvingbitcoin.org/t/hornet-update-a-declarative-executable-specification-of-consensus-rules/2420 "2026-04-15T22:46:48Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![tobysharp](https://delvingbitcoin.org/letter_avatar_proxy/v4/letter/t/dbc845/32.png) [@tobysharp](https://delvingbitcoin.org/u/tobysharp)\
**Post date:** [April 15, 2026, 10:46pm UTC](https://delvingbitcoin.org/t/hornet-update-a-declarative-executable-specification-of-consensus-rules/2420/1 "2026-04-15T22:46:48Z")

</div>

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](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 [hornet/src/hornetlib/consensus/rules/spec.h at main · tobysharp/hornet · GitHub](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](https://hornetnode.org/spec.html).

To read more about Hornet and how it relates to other projects, see [https://hornetnode.org/overview.html](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:

```auto
// 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.

---

<div class="post-metadata">

**Author:** ![Laz1m0v](https://delvingbitcoin.org/user_avatar/delvingbitcoin.org/laz1m0v/32/1951_2.png) [@Laz1m0v](https://delvingbitcoin.org/u/Laz1m0v)\
**Post date:** [April 15, 2026, 11:02pm UTC](https://delvingbitcoin.org/t/hornet-update-a-declarative-executable-specification-of-consensus-rules/2420/2 "2026-04-15T23:02:34Z")

</div>

Hi Toby. There is immense value in this. Your approach to treating consensus validity as a pure, side-effect-free boolean function perfectly mirrors our own architectural philosophy at the covenant and transaction derivation layer.

While Hornet formalizes node-level block consensus, our recent work on the PRECOP framework formalizes transaction topology and covenant execution. We rely on Simplicity to enforce deterministic, fail-closed state transitions, shifting from “passive verification” to mathematical necessity.

Regarding your future work on rule S06 (Script rules): this is precisely the frontier. We are currently upstreaming native Bitcoin introspection jets into `rust-simplicity` to ensure that script evaluation and economic invariants can be formally verified without relying on external witnesses.

The convergence of a declarative node consensus (Hornet) and a deterministic covenant execution environment (PRECOP/Simplicity) is exactly how we harden Bitcoin’s base layer. Excellent initiative, we will be watching your progress closely.