The Myth of the Valid Transaction

You hear it all the time: the phrase “valid transaction”.

I’ve used this phrase on countless occasions myself. When Bitcoin developers use it, we’re usually talking about whether a transaction obeys Bitcoin’s consensus rules.

There’s only one problem with it. There’s no such thing as a “valid transaction”.

This sounds silly, but accepting this frame makes it easier to reason about Bitcoin’s behavior. Before I can justify that, though, I need to explain what I mean. Bitcoin obviously has rules governing transactions, and Bitcoin Core does perform consensus-critical checks on every transaction when deciding whether to accept a block. So what exactly am I claiming does not exist?

I am claiming that “validity” is not really a property of a transaction. This phrase makes it sound as though validity is something that can be decided about transactions, the same way we can read their version or count their inputs and outputs. If we have the transaction, this language suggests we should be able to determine whether it is valid.

My last post introduced btc-verified, an attempt to formalize Bitcoin’s protocol semantics in Lean. When you formalize a statement, any context hidden by ordinary language eventually has to become an explicit input to some definition. If validity really belongs to the transaction, what would that definition look like?

You might try something like this:

isValid : Tx → Bool

At first glance, this seems perfectly sensible. There are quite a few things we can determine from a transaction alone. It needs inputs and outputs. It cannot spend the same outpoint twice. Its output values and stripped serialized size have to stay within certain bounds. Bitcoin Core groups these together in CheckTransaction. Taken together, these checks appear to give us the definition we were looking for.

There’s a problem with it, though. One of the central goals of Bitcoin is to solve the double spend problem. We have to ensure that the inputs to the transaction have not been spent, and therefore we have to ensure they exist in the UTXO view against which the transaction is being evaluated. If we don’t have access to that view when making the decision, how can we possibly solve the problem?

Perhaps we can add an argument for it to the predicate:

isValid :
  (utxos : UtxoSet) →
  (tx : Tx) →
  Bool

This gets us closer, but we still have an issue.

Transactions enter consensus history only as part of blocks. Each block contains one or more transactions, and if we ran a check like this independently for each of them, two transactions spending the same output could both pass. If we don’t compute the resulting UTXO set after every transaction, a block could contain a double spend.

It was at this time in my attempt to implement the consensus rules that I realized it didn’t make sense to think about the consensus rules as something that applied to transactions at all. The protocol-level decision is whether a candidate block validly extends a particular parent state; a transaction’s admissibility is merely one step within that single atomic decision.

Within each block, an admissible transaction must operate on the UTXO set before we can safely evaluate the next one. This same transition also allows a later transaction to consume an output created by an earlier one.

For every block this means we have a transaction-level state transition that looks closer to this:

applyTransaction :
  (utxos : UtxoSet) →
  (tx : Tx) →
  Option UtxoSet

This transition evaluates the transaction’s admissibility and, on success, updates the UTXO set. The resulting set becomes the argument to the next transaction’s decision.

If the UTXO set were the only context needed to evaluate a transaction, folding this transition over the block would tell the whole story. It isn’t. Consider a transaction with an absolute lock time. Core’s function for deciding whether that condition is satisfied takes the transaction, a block height, and a block time. It also inspects the input sequence numbers, which may override the lock. The IsFinalTx interface makes these dependencies explicit, and BIP113 changed the supplied time without changing the function itself. The same transaction can fail this condition for one candidate block and satisfy it for a later one.

So what will the full transition need to know?

btc-verified does not implement this complete block transition yet. A sketch of the interface it is working toward, exposing the history-dependent inputs used in the discussion so far, looks like this:

applyBlock :
  (utxos : UtxoSet) →
  (height : Nat) →
  (medianTimePast : Nat) →
  (block : Block) →
  Option UtxoSet

The block carries its own header time, but its prospective height and the preceding chain’s median time past come from the history it claims to extend. Along any candidate chain, each accepted block takes us from a parent state to a child state. Inside that attempted block transition, the transactions update a temporary view of the UTXO set in order. There is a block-level fold of history, with a transaction-level fold inside each block.

Bitcoin Core makes this same distinction in its implementation. ConnectTip applies a block atomically to chainstate, while ConnectBlock walks through its transactions and updates a temporary coin view. The inner transition is consensus-critical: changing it can change which blocks an implementation accepts or the state produced by an accepted block.

Does that make the transaction transition a separate consensus object in its own right?

Not quite. Those intermediate UTXO sets do not independently enter Bitcoin’s history. An implementation can factor the work differently, or choose not to expose a separately named transaction transition at all, provided that it accepts the same block extensions and produces the same observable state. The formal unit of consensus is the block extension. Transaction checks and state changes are premises inside that judgment.

But don’t Bitcoin nodes accept and reject individual transactions all the time?

They do, but this is a mempool decision. Core’s normal standalone-transaction path attempts mempool admission, not a chainstate update. Nodes can have different mempools, different relay policies, or no mempool at all while remaining in consensus about the ledger. A transaction changes consensus chainstate only when it appears in a block the node connects.

If isValid : Tx → Bool is not the consensus judgment, was it simply the wrong place to start?

No. It asks useful questions under an overloaded name. In btc-verified, transaction-local questions are handled by Tx.isWellFormed. It checks that a regular transaction has inputs and outputs, does not spend the same outpoint twice, does not claim the null outpoint, and stays within the value and stripped-size bounds. The project proves that this executable check agrees exactly with a proposition stating those premises.

The name is deliberate. A well-formed transaction is not necessarily one that can appear at a particular point in a block. For that, btc-verified has Tx.isAdmissible, which takes the UTXO set, block context, a selected lock-time clock, and an abstract script judgment as inputs.

Even the transaction’s fee crosses this boundary. A transaction records the values of its outputs, but the values of its inputs live in the outputs being spent. The fee appears only after those inputs are resolved against a particular UTXO set and the value created is subtracted from the value consumed. “Transaction fee” is another useful compression that hides part of the calculation.

Are these distinctions limited to the consensus checks themselves?

No. I made the same category error at the parsing boundary in btc-verified’s original transaction type. Since an ordinary transaction must have an input, the type required every transaction value to have one. If a transaction with no inputs can never be admitted into a block, why represent it?

Because parsing is not validation.

Core’s witness-aware decoder can construct the degenerate object with no inputs and no outputs. The decoder admits the object, while CheckTransaction rejects its empty input list.

An earlier version of btc-verified made nonempty inputs an invariant of its transaction type. Its parser could handle ordinary SegWit transactions, but it could not represent the empty object admitted by Core’s decoder. Correcting the model required changing Tx to represent that object and moving input existence into the transaction-local premises.

A parser may reject that object and still recognize every consensus-valid transaction, but it would not model the full domain of Core’s decoder. Because btc-verified aims to remain compatible with Core at observable boundaries, parsing and validation cannot be allowed to collapse into one another.

What does separating all of these judgments buy us?

These distinctions are not merely pedantic. The boundaries we choose in an implementation determine how cleanly it matches the reality of the protocol.

When parsing, policy, contextual checks, and consensus are collapsed into a single idea of validity, the mismatch first reappears as friction somewhere else in the system: special cases, awkward interfaces, or assumptions that callers have to remember because the software cannot express them. That friction is almost always what comes before something breaks. By the time the mismatch becomes a bug, other code may already depend on the faulty boundary, making it far more expensive to correct. It is much cheaper to fix the mental model when the first friction appears.

The transaction-local and contextual checks now guard btc-verified’s internal regular-transaction transition, applyChecked. For a transaction that satisfies both sets of premises, btc-verified proves an accounting identity relating the prior state, the spent value, the created value, and the resulting state. It follows that an ordinary transaction cannot increase the total value held in the UTXO set. Once admissibility and the state transition are explicit, conservation stops being an assumption bundled into the word “valid” and becomes a theorem about the resulting UTXO set.

There is an important caveat here. btc-verified does not yet implement the complete valid-block-extension judgment. Script remains an abstract parameter, while relative lock times and the height-indexed active-ruleset mapping remain to be modeled. The project currently stops at the reusable premises and guarded transition for ordinary transactions. The block fold, coinbase handling, and block-wide conditions are the next layer, not something already proved by the transaction work. Even after those pieces are finished, none of them will make validity an intrinsic property of a transaction.

So where does that leave the phrase “valid transaction”?

I don’t think we have to stop using it. Engineers need compressed language, and “valid transaction” carries a great deal of shared context cheaply. But when we move from conversation to a specification, the compression has to be expanded.

When we call a transaction valid, we mean that it satisfies some transaction-local premises and, in a particular position in a particular block, under the rules active for the history that block extends, does not cause the block transition to fail. That is far too much context to repeat in ordinary conversation, which is exactly why the shorter phrase will survive.

But the longer formulation is the one we have to prove.

At the consensus boundary, there is no valid transaction floating free of a history. There is only a candidate block, the history it claims to extend, and the consequences of accepting it.