Blockchain
Open Problems and Research
In 2024, Vitalik Buterin published an updated Ethereum roadmap - and honestly admitted: half the items are marked "active research", with no guarantees of resolution. Sharding? Six years of work, three strategy changes, the result - EIP-4844 with blobs instead of the promised 64 shards. MEV? Flashbots created MEV-Boost, but 90% of blocks are built by two builders - centralization instead of a solution. Privacy? Tornado Cash is under sanctions, and FHE is 10,000 times slower than regular computation. Formal verification? Costs millions, while bug losses are in the billions. The blockchain industry stands at the edge of problems that have no answers yet. This lesson is a map of the territory where engineering ends and science begins.
- **Ethereum Danksharding** - the shift from execution sharding to data sharding after recognizing that atomic composability for 64 shards is an unsolvable problem in its current form
- **Flashbots SUAVE** - an attempt to create a separate blockchain for MEV auctions, because existing solutions (MEV-Boost) centralized block building to 2-3 dominant builders
- **Zama fhEVM** - Fully Homomorphic Encryption for EVM, enabling computation over encrypted data, but with ~1000x overhead - on the edge of practical viability
Предварительные знания
Sharding: Unsolved Scaling Problems
Sharding promises horizontal scaling of blockchains - split the network into parallel "shards", each processing its own slice of transactions. It sounds simple: 64 shards = 64x throughput. In practice, however, sharding spawns an entire family of problems, many of which **still lack satisfactory solutions**. After six years of research, Ethereum abandoned execution sharding in favor of danksharding - and even that path is full of open questions.
**Atomic composability** - the fundamental problem of cross-shard transactions. In a monolithic blockchain, DeFi protocols freely call each other within a single transaction: swap on Uniswap → deposit in Aave → borrow → hedge on dYdX. It is all atomic - either executed in full or rolled back entirely. In a sharded network, contracts live on different shards. A cross-shard call is an **asynchronous message**, not an atomic operation. The first part can succeed, the second can fail, and rolling back the first is no longer possible.
**Single-Slot Finality (SSF)** - another open problem. Currently Ethereum achieves finality in ~15 minutes (2 epochs). SSF promises finality within a single slot (~12 sec), but requires **all** ~1 million validators to vote within one slot. Current BLS aggregation cannot handle that volume of signatures. Research is exploring **signature aggregation** (SNARK-based aggregation), **committee rotation** (a subset of validators), and **orbit SSF** (Buterin, 2024) - but none of these approaches has yet proven production-ready.
**State growth** - a slow-moving catastrophe. A full Ethereum node stores >300 GB of state, and that volume grows with every block. Without a solution, in 5-10 years only data centers will be able to run nodes, which kills decentralization. Two research directions: **state expiry** (data not accessed for N epochs "sleeps" and requires a witness to reactivate) and **statelessness** (nodes do not store state but receive a witness with every block). Statelessness requires **Verkle trees** - a replacement for the Merkle Patricia Trie that reduces proof size from ~4 KB to ~200 bytes. Ethereum's migration to Verkle trees is one of the most significant engineering undertakings in blockchain history.
**Verkle trees** - a hybrid of **Vec**tor commitments and Me**rkle** trees (hence the name). They use polynomial commitments (IPA or KZG) instead of hashing, which drastically reduces proof size. Ethereum plans to transition from MPT to Verkle, but the migration requires simultaneously updating the state format, proof generation, and all clients - a process that will span several hard forks.
Why is atomic composability a fundamental problem with sharding, not simply an engineering challenge?
MEV: An Existential Problem and Paths to Resolution
**Maximal Extractable Value (MEV)** - the profit a block producer can extract by reordering, inserting, or censoring transactions in a block. MEV is not a bug but a **fundamental property** of systems where the order of transactions matters. Every unprotected DEX swap is an opportunity for a sandwich attack. Every liquidation is a bot race. According to Flashbots estimates, more than $600M in MEV has been extracted on Ethereum alone since the Merge. But the problem goes deeper: MEV threatens the **very foundations** of blockchain - decentralization, censorship resistance, and fairness.
Why is MEV an **existential** problem? Because it creates a centripetal force. The more MEV there is, the more profitable it is to be a large validator with powerful infrastructure. Large players extract more MEV → stake more → extract even more MEV. The result: **centralization of the validator set**, which undermines the core promise of blockchain. Furthermore, MEV bots pollute the mempool with spam - ~30% of Ethereum's gas is spent on failed MEV transactions.
**Proposer-Builder Separation (PBS)** - an architectural solution: separate the roles of the party that **proposes** a block (proposer) and the party that **builds** it (builder). The proposer selects a builder by bid without knowing the block's contents. The builder extracts MEV but competes with other builders, passing most of the profit to the proposer. Currently PBS works through **MEV-Boost** (Flashbots) - an out-of-protocol mechanism. Ethereum is researching **enshrined PBS** - embedding PBS into the protocol to remove the dependency on Flashbots. But enshrined PBS raises new questions: how to prevent builder centralization? How to enforce inclusion lists?
**MEV-Burn** - a radical proposal (Justin Drake, 2023): instead of redistributing MEV, **burn** it. The builder pays a bid for the right to build a block, and that bid does not go to the proposer but is **destroyed** - ETH leaves circulation permanently. This removes the incentive for proposers to choose builders based on MEV, making the system fairer. However, MEV-burn does not solve the censorship problem - a builder can still exclude unwanted transactions.
**Inclusion lists** - a censorship-resistance mechanism for PBS. The proposer publishes a list of transactions that the builder **must** include in the block. If the builder refuses - the block is invalid. This prevents builders from censoring transactions (e.g., OFAC-sanctioned addresses). The challenge: how large should the inclusion list be? Too small - useless. Too large - the builder cannot optimize the block. An active area of research (FOCIL - Fork-Choice enforced Inclusion Lists).
Encrypted mempools (threshold encryption) completely solve the MEV problem. What is wrong with this claim?
Privacy and Scalability: An Impossible Trade-off?
Blockchain is transparent by design: every transaction, every balance, every contract call - all public. For DeFi this means **your entire financial profile is exposed**. Anyone can see how much ETH you have, what positions you hold in Aave, and when you sold. For enterprise use cases this is a showstopper. But adding privacy to blockchain is one of the most difficult open problems, because privacy **conflicts** with scalability, compliance, and the smart-contract model itself.
ZK-proofs solve two entirely different problems: **ZK for scaling** (ZK-rollups) proves the correctness of computations without re-executing them on L1 - but the data itself remains public. **ZK for privacy** (Zcash, Aztec) hides transaction data - sender, recipient, amount - publishing only a validity proof. Combining both properties (scaling and privacy) is the key goal of projects like Aztec Network, but the computational cost of ZK-proofs for private computations is orders of magnitude higher than for public ones.
**MPC (Multi-Party Computation)** - an alternative approach: multiple parties jointly compute a function without any of them seeing the others' inputs. For DeFi this means: multiple nodes jointly execute a swap, each knowing only its own share. Projects: **Partisia Blockchain** (MPC for smart contracts), **Nillion** (blind compute network). Trade-off: MPC requires communication between participants during computation - O(n^2) messages for n participants, which limits scalability.
**Frontier:** ZK + FHE + MPC - convergence of technologies. Imagine a system where FHE provides an encrypted state, a ZK-proof confirms the correctness of computations over that encrypted data, and MPC distributes the decryption key. Each technology covers the weakness of another. Projects like **Sunscreen** and **Zama** are already exploring such hybrids. But the computational cost of combined schemes is currently prohibitive - this is an area where hardware acceleration (GPU, FPGA, ASIC) will be the deciding factor.
What is the key difference between "ZK for scaling" and "ZK for privacy"?
Formal Methods: Mathematical Guarantees of Correctness
In 2016, the DAO hack lost $60M due to a reentrancy bug - an error that formal analysis could have caught. In 2022, the Wormhole bridge lost $320M due to a missed signature check. Ronin Bridge - $625M. **Total losses from smart-contract bugs exceed $5 billion**. Formal methods are a mathematical toolkit for **proving** the correctness of code, not merely testing it. But their application in blockchain faces unique challenges: scale, cost, and the gap between academia and industry.
**Formal verification** - proof that a program meets its specification for **all** possible inputs. Not 1,000 tests, not 1 million - a **mathematical guarantee** for an infinite set. In the context of smart contracts: prove that "under no circumstances can more tokens be withdrawn than were deposited." This requires: 1. a formal specification - what the program should do 2. a formal model - what the program actually does, and (3) a proof - that the model matches the specification.
**TLA+ (Temporal Logic of Actions)** - Leslie Lamport's specification language, used for formal verification of distributed systems. Amazon uses TLA+ for DynamoDB and S3. In blockchain: **Informal Systems** verified the Tendermint consensus in TLA+, discovering a bug in the algorithm that thousands of hours of testing had missed. **Apalache** - a model checker for TLA+ that automatically checks specifications. The caveat: TLA+ describes a **model** of the system, not the code itself - a separate step is needed to prove that the code matches the model.
**The cost-benefit paradox of formal methods:** verifying a single smart contract costs $500K-5M and takes 3-12 months. For a startup launching a DeFi protocol - that is prohibitive. Yet the cost of a vulnerability is tens or hundreds of millions. Several research directions are addressing this: **automated verification tools** (Certora Prover, Halmos) reduce cost to days instead of months; **verified libraries** (OpenZeppelin) let you build from already-proven components; **certified compilers** (KEVM) guarantee that if the source code is correct, the bytecode is correct too.
**Model checking for consensus:** Tendermint, Ethereum Casper, Avalanche - all these consensus protocols had bugs discovered through formal analysis. In 2019, a TLA+ specification of Tendermint revealed an edge case in the algorithm where two-thirds of validators could finalize conflicting blocks under a specific sequence of timeouts. The bug had existed for years and was never caught by tests. Formal verification of consensus protocols is one of the few areas with a directly positive cost-benefit ratio: the price of a failure is losing the entire network.
Formal verification of smart contracts guarantees the complete absence of bugs and makes audits unnecessary. If a contract is verified in Coq - it is absolutely secure.
Formal verification proves that **code matches its specification** - but does not guarantee that **the specification is correct**. If the specification fails to account for an economic attack (flash loan manipulation), governance attack, or oracle manipulation - the verified code will be "correctly" vulnerable. Moreover, verification only covers formalized properties - unformalized aspects (UX, gas optimization, upgradeability) remain out of scope.
The DAO hack is the example: the code worked "per spec" (withdraw is called before balance update), but the spec did not formalize the invariant "withdraw cannot be called recursively." Formal methods are a powerful tool, not a silver bullet. They complement (not replace) audits, testing, and bug bounties. The best strategy is defense in depth: static analysis + formal verification of critical invariants + runtime monitoring + audit.
Informal Systems discovered a bug in Tendermint consensus through a TLA+ specification. Why was this bug not found by tests?
Key Takeaways
- **Sharding** promises horizontal scaling, but atomic composability (cross-shard transactions), single-slot finality, and state growth (~300 GB) remain unsolved. Ethereum switched strategy to danksharding, and the transition to Verkle trees for statelessness is an engineering challenge spanning years
- **MEV** is not a bug but a fundamental property of systems where transaction ordering matters. Encrypted mempools, PBS, SUAVE, fair ordering - each approach solves part of the problem, but none eliminates MEV entirely. MEV-burn proposes burning rather than redistributing the extracted value
- **Privacy** conflicts with scalability and compliance. ZK for privacy, FHE (computation over encrypted data), MPC - three approaches with different trade-offs. Privacy pools (Buterin, 2023) seek a middle ground between anonymity and regulatory requirements
- Remember Buterin's roadmap marked "active research"? **Formal methods** - from static analysis to theorem proving - are the only path to mathematical correctness guarantees, but the cost of verification ($500K-5M) creates a paradox: expensive to verify, yet even more expensive not to verify given $5B+ in losses
Related Topics
The open problems of blockchain connect the foundational concepts studied earlier:
- Data Availability — DAS (Data Availability Sampling) - a key component of danksharding, determining how nodes verify data availability without downloading the full dataset
- MEV: Maximal Extractable Value — The foundation for understanding the MEV problem - sandwich attacks, frontrunning, searchers and builders that MEV mitigation aims to neutralize
- Zero-Knowledge Proofs: Fundamentals — ZK-proofs underpin both scaling (ZK-rollups) and privacy (Zcash, Aztec) - two applications of the same technology with different trade-offs
- Formal Verification — The foundational concepts of formal methods - invariants, pre/post-conditions, model checking - that scale up to verifying entire protocols
Вопросы для размышления
- Ethereum abandoned execution sharding in favor of danksharding (data sharding + L2 for execution). Does this mean the idea of sharding state and execution is fundamentally a dead end - or does it simply require technologies that don't yet exist (e.g., ZK for cross-shard composability)?
- MEV-burn proposes burning MEV instead of redistributing it. But if MEV is burned, searchers and builders have no incentive to optimize transaction ordering. Could this lead to a less efficient market? Is there an "optimal" level of MEV?
- FHE enables computation over encrypted data but with ~1000x overhead. Moore's Law predicts doubling of performance every 2 years. How many "Moore generations" are needed for FHE to become practical? Or is a fundamentally different approach required (FHE-ASIC, quantum computing)?