arXiv subjects

Tobias Klenze

Publications and source records attributed to Tobias Klenze.

5 recordsLinked to original sources

arXiv2026

MonadBFT: Fast, Responsive, Fork-Resistant Streamlined Consensus

This paper introduces MonadBFT, a novel Byzantine Fault Tolerant (BFT) consensus protocol that advances both performance and robustness. MonadBFT is implemented as the consensus protocol in the Monad blockchain. As a HotStuff-family protocol, MonadBFT has linear message complexity in the common case and is optimistically responsive, operating as quickly as the network allows. A central feature of MonadBFT is its tail-forking resistance. In pipelined BFT protocols, when a leader goes offline, the previous proposal is abandoned. Malicious leaders can exploit this tail-forking behavior as a form of Maximal Extractable Value (MEV) attack by deliberately discarding their predecessor's block, depriving that proposer of rewards and enabling transaction reordering, censorship or theft. MonadBFT prevents such tail-forking attacks, preserving both fairness and integrity in transaction execution. Another related feature of MonadBFT is its notion of speculative finality, which enables parties to execute ordered transactions after a single round (i.e., a single view), with reverts occurring only in the rare case of provable leader equivocation. This mechanism reduces user-perceived latency. Additionally, we introduce the leader fault isolation property, which ensures that the protocol can quickly recover from a failure. To our knowledge, no prior pipelined, leader-based BFT consensus protocol combines all of these properties in a single design.

cs.DC↗

arXiv2026

Cadence: Extreme Pipelining with Multiple Concurrent Proposers

We present Cadence, a Byzantine fault-tolerant multi-proposer consensus protocol with arbitrarily low block intervals, optimal resilience, and optimal fast-path latency. Cadence divides time into equally spaced slots, one block per slot, each finalized in its own consensus instance. Blocks do not build directly on their predecessor, so instances run independently and none waits for an earlier block to finish or propagate; we call this extreme pipelining, decoupling the block interval from network latency. Cadence also removes the single-leader monopoly over transaction inclusion and ordering: under multiple concurrent proposers (MCP), several validators propose for each block, and it guarantees that, under synchrony, a transaction a correct proposer includes cannot be censored or deferred (short-term censorship resistance), and that no proposer can craft its proposal in reaction to the others' (hiding). To realize extreme pipelining, we introduce a general framework that turns any one-shot consensus meeting our slot-consensus specification into a multi-shot protocol. We instantiate it for MCP with two protocols of our own: Chorus, a slot consensus whose fast path finalizes a block in an optimal three rounds, with speculative finality one round earlier, and Conductor, an orchestrator that opens slots at an even cadence, more slowly under asynchrony to keep open slots bounded. To our knowledge, Cadence is the first MCP protocol to provide short-term censorship resistance and hiding at the fast-path latency of single-leader consensus. We prove safety, liveness, censorship resistance, and hiding under partial synchrony with optimal resilience (n = 3f+1). In simulation over Monad's 200 validators with five proposers per slot, finalization averages 219 ms (167 ms to speculative finality); at a 100 ms block interval a transaction waits on average 50 ms to enter a proposal.

cs.DC↗

arXiv2024

A New Broadcast Primitive for BFT Protocols

Byzantine fault tolerant (BFT) protocol descriptions often assume application-layer networking primitives, such as best-effort and reliable broadcast, which are impossible to implement in practice in a Byzantine environment as they require either unbounded buffering of messages or giving up liveness, under certain circumstances. However, many of these protocols do not (or can be modified to not) need such strong networking primitives. In this paper, we define a new, slightly weaker networking primitive that we call abortable broadcast. We describe an implementation of this new primitive and show that it (1) still provides strong delivery guarantees, even in the case of network congestion, link or peer failure, and backpressure, (2) preserves bandwidth, and (3) enforces all data structures to be bounded even in the presence of malicious peers. The latter prevents out-of-memory DoS attacks by malicious peers, an issue often overlooked in the literature. The new primitive and its implementation are not just theoretical. We use them to implement the BFT protocols in the IC (Internet Computer), a publicly available blockchain network that enables replicated execution of general-purpose computation, serving hundreds of thousands of applications and their users.

cs.NI↗

arXiv2024

Protocols to Code: Formal Verification of a Next-Generation Internet Router

We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol's network-wide security properties and low-level properties of its implementation. More precisely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router's Go code satisfies memory safety, crash freedom, freedom from data races, and adheres to the protocol model. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol's security properties. This paper explains our approach, summarizes the main results, and distills lessons for the design and implementation of verifiable systems, for the handling of continuous changes, and for the verification techniques and tools employed.

cs.CR↗

arXiv2020

Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification

Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have demonstrated that full verification of entire systems is feasible by establishing a refinement relation between an abstract system specification and an executable implementation. Existing approaches however impose severe restrictions on either the abstract system specifications due to their limited expressiveness or versatility, or on the executable code due to their reliance on suboptimal code extraction or inexpressive program logics. We propose a novel methodology that combines the compositional refinement of abstract, event-based models of distributed systems with the verification of full-fledged program code using expressive separation logics, which support features of realistic programming languages like mutable heap data structures and concurrency. The main technical contribution of our work is a formal framework that soundly relates event-based system models to program specifications in separation logics, such that successful verification establishes a refinement relation between the model and the code. We formalized our framework, Igloo, in Isabelle/HOL. Our framework enables the sound combination of tools for protocol development with existing program verifiers. We report on three case studies, a leader election protocol, a replication protocol, and a security protocol, for which we refine formal requirements into program specifications (in Isabelle/HOL) that we implement in Java and Python and prove correct using the VeriFast and Nagini tools.

cs.LO↗