Blockchain is a highly adversarial environment. Anything with value and an exposed surface is being probed by increasingly capable adversaries. Implementation correctness is existential.

In Finding Bugs that Frontier Models Miss, we explored how formal verification can prove that an implementation satisfies specified properties. While LLMs have reduced the cost of producing both proofs and software, they have not eliminated every bottleneck. Specifying the system remains cognitively expensive: deciding which properties must be proven and whether those properties adequately capture the intended behavior.

A specification can support more than formal proof. It can also be used to derive a reference implementation, or model, that serves as a test oracle. Typically, this implementation is simpler than the production code, because its purpose is to express the specified behavior, not to optimize performance. Any divergence between the model and implementation yields a concrete counterexample, potentially exposing an implementation bug, a model error, or a missing invariant.

Staking Folklore

Staking is a ubiquitous feature of blockchains. If it works, nobody notices. If it fails, everyone notices. While staking designs differ from chain to chain, they generally share common features and requirements:

1. Escrowed assets - user assets earn rewards for participation in consensus.
2. Epoch-specific validator set - a definition of the validator set and its lifetime in consensus.
3. State changes to the validator set - rules for how actors can alter the validator set.
4. Delegation - a mechanism allowing users to contribute stake without operating a validator.

One of the worst possible failures is an “infinite mint” bug. This occurs when an attacker can create an arbitrary amount of tokens. On the Monad blockchain, new MON can only be minted as block rewards, which are attributable to stakers. The staking precompile is therefore one critical point where an “infinite mint” vulnerability could occur.

Staking designs with delegation have historically assumed consensus and execution run in lockstep. Monad relaxes this assumption with asynchronous execution to accommodate much higher throughput. The resulting interaction creates an interesting two-body problem.

Two-Body Problem

Monad represents the march of time as increasing block numbers. A fixed span of blocks defines an epoch. An epoch defines the lifetime of a particular validator set. However, consensus and execution advance asynchronously. This presents our two-body problem: consensus can enter a new epoch while execution is still processing blocks from the previous one. Therefore, the system must define when changes in execution can be applied to consensus.

From execution’s point of view, the current state is defined by the most recently processed block. This view advances one block at a time. The diagram below shows this view, with each epoch spanning an interval of consecutive blocks.

Let d and d' be the first blocks of epoch n and epoch n + 1. The difference between the consensus and execution viewpoints is bounded by k blocks, where k is a system parameter. By the time consensus reaches block d', execution is guaranteed to have processed the state at block d' - k. The validator set for epoch n + 1 can therefore be determined from the state before this point. Any changes to the validator set after this point must wait until at least the next epoch, and the corresponding stake must therefore remain escrowed until it is no longer active in consensus. The highlighted blue region in the diagram above represents this window.

Delegation and Specifications

Monad’s delegation mechanism allows a single validator to collect rewards on behalf of many delegators. As a result, reward accounting scales with the number of validators rather than the (much larger) number of delegators, and delegators are entitled to a pro rata share of rewards. But this efficiency creates two related accounting obligations:

1. At the validator level, aggregate stake must remain backed by the underlying delegator positions.
2. At the account level, the staking account’s assets must equal its total outstanding liabilities.

These are the staking solvency invariants. They must hold after every state transition. Otherwise, the account can become under-collateralized.

$$ \begin{aligned} s.&\mathtt{balance\_of}(\mathtt{STAKING\_CA}) = \\ & \Big( \sum_{v \in \mathtt{uint64}} s.\mathtt{val\_execution}(v).\mathtt{stake} \Big) + \\ &\Big( \sum_{v \in \mathtt{uint64}} s.\mathtt{val\_execution}(v).\mathtt{unclaimed\_rewards} \Big) + \\ &\Big( \sum_{v\in \mathtt{uint64}, a \in \mathtt{address}} s.\mathtt{delegator}(v, a).\mathtt{rewards} \Big) + \\ &\Big( \sum_{v\in \mathtt{uint64}, a \in \mathtt{address}, i \in \mathtt{uint8}} s.\mathtt{withdrawal\_request}(v, a, i).\mathtt{amount} \Big) \end{aligned} $$

The specification of staking gives a well-defined description of the system. It was developed by reconciling the behavior of the implementation with the intended behavior of the system. It models each operation as a state transition and states the invariants that every reachable state must preserve. The account level invariant is shown above and the complete specification of the staking model, including the validator level invariant, is available here.

Empirical Verification

The primary goal was to establish high confidence that the solvency invariants were preserved. This required two forms of empirical evidence:

1. Exercise each logically distinct state transition and its corresponding implementation paths for a given property. This provides evidence that no relevant code path was omitted.
2. Generate a large corpus of valid operation sequences and check the solvency invariants after every transition. This provides evidence that the invariants hold across a broad sample of reachable states.

To gather both forms of evidence, we developed a reference implementation from the spec together with a stateful fuzzer. A naive generator would waste effort on trivial or redundant operation sequences and rarely reach important cases. Instead, the stateful fuzzer biased its choices toward specific numerical and epoch boundaries. After each operation, we advanced both the model and the implementation, then compared their observable state and checked solvency. Any disagreement produced a counterexample that became a regression test once the discrepancy was understood and corrected.

We then used mutation testing to evaluate the harness’s state coverage. Guided by the model’s logic, we injected known bugs into the implementation and checked whether the fuzzer reached each targeted path and whether the comparison detected the difference once there. A surviving mutation exposed a gap in the generator or the model. A detailed example is shown in the next section.

Together, these results provided concrete evidence both that the targeted paths were exercised and that the specified invariants held throughout the generated executions.

Closing a Coverage Gap

The following mutation initially survived because the generator did not create enough validators to cross the first 256-ID bitset boundary:

--- a/category/execution/monad/staking/staking_contract.hpp
+++ b/category/execution/monad/staking/staking_contract.hpp
@@ -224,7 +224,7 @@ public:
                 uint8_t slots[23];
             } key{
                 .ns = Namespace::ValBitset,
-                .bucket = (val_id.native() >> 8),
+                .bucket = (val_id.native() >> 9),
                 .slots = {}};

             return {state_, STAKING_CA, std::bit_cast<bytes32_t>(key)};

We revised the generator so that, with low probability, it creates 260 validators, enough to cross the first bucket boundary. Crossing it made the incorrect bucket calculation observable, and the fuzzer quickly detected it.

The same change caught other mutations requiring larger validator IDs, including one that incorrectly aliased bit positions 128–255 onto positions 0–127:

--- a/category/execution/monad/staking/staking_contract.cpp
+++ b/category/execution/monad/staking/staking_contract.cpp
@@ -625,7 +625,7 @@ bool StakingContract::add_to_valset(u64_be const val_id)
 void StakingContract::remove_from_valset(u64_be const val_id)
 {
     uint256_t set = vars.val_bitset_bucket(val_id).load().native();
-    uint256_t const mask = ~(1_u256 << (val_id.native() & 0xFF));
+    uint256_t const mask = ~(1_u256 << (val_id.native() & 0x7F));
     set &= mask;
     vars.val_bitset_bucket(val_id).store(set);
 }

Thus, a surviving mutation identified a specific missing boundary case and directly informed an improvement to the generator.

Conclusion

This post considered an instance of a general problem: how do we show that a piece of software does what we intend? No single method settles this question. At Category Labs, we use a wide range of tools to secure the Monad client, including formal verification and model-based fuzzing. Both begin with the same essential task: defining what correctness means.

For staking, solvency was the primary concern. Making that notion precise required reconciling the intended design with the behavior of the implementation. Once solvency was specified, the reference implementation became an oracle, producing an inspectable chain of evidence that the production implementation preserved solvency across the explored states.

Attributions

Andreas Lynge derived the formal specification and designed and implemented the testing methodology described above. Matt Kolosick also helped implement the harness and debug fuzzer output. John Bergschneider, Kevin Kuehler, and Bharath Amrithraj designed and implemented the staking module.

Links

1. Full specification of the staking contract - https://category-labs.github.io/category-research/Staking_Spec.pdf
2. Implementation of the executable model and the staking test harness - https://github.com/category-labs/monad/tree/main/category/execution/monad/staking/fuzzer