As a DeFi user, continuously exploring new narratives and testing emerging protocols like EigenLayer and Pendle, I became increasingly curious about the safety and risk management aspects of these investments. This curiosity led me to dig deeper into understanding how the code underlying the leading DeFi protocols (AAVE, Compound, MakerDAO, etc) safeguards users’ assets.

This article explores formal verification, a method that mathematically proves system correctness, and how it can significantly enhance security in DeFi protocols. It is particularly relevant for:

• Blockchain developers looking to enhance their code security practices

• DeFi power users and investors who want to understand auditing and general fund security measures

• Protocol operators seeking to improve their security infrastructure

• Governance committee members who need to make informed decisions about protocol upgrades and security measures

• Auditors looking to expand their toolkit with formal verification methods

• Researchers, educators, and students interested in advanced security techniques for cybersecurity and blockchain

• Regulatory bodies and insurance providers in the DeFi space who need to understand and assess protocol risks

This article offers an in-depth look at formal verification in DeFi. As it’s a bit of a long read, here’s a friendly guide to help you navigate the content, with notes on who might find each section most relevant:

• The Limitations of Traditional Testing: Explores why conventional testing methods might not be enough for DeFi protocols. For all readers, especially those new to DeFi security.

• The Case for Formal Verification: Introduces how mathematical proofs can enhance smart contract security. For DeFi users, investors, and anyone curious about improving protocol safety.

• Formal Specifications and Symbolic Variables: Explains the building blocks of formal verification in simple terms. For developers and technically inclined readers.

• Practical Example: From Code to Proofs: Walks through a step-by-step verification process, great for those who love technical details. For developers, researchers, and those deeply interested in the mechanics.

• Certora Prover: Showcases a powerful tool that automates formal verification for smart contracts. For developers and protocol teams considering implementation.

• Challenges and Applicability: Discusses where formal verification fits in the DeFi landscape and its current limitations. For protocol operators, governance members, and researchers.

• The Interconnected Nature of Security Measures: Puts formal verification in context with other security practices. For all stakeholders to understand the bigger security picture.

• The Importance of Reputable Verification: Offers tips for evaluating the security of DeFi protocols you might use or invest in. For DeFi users and investors.

• Conclusion and Resources: Wraps up key points and suggests further reading for the curious. For all readers, with resources for those wanting to dive deeper.

We can all contribute better to a safer DeFi ecosystem by understanding formal verification and advanced security practices.

The Limitations of Traditional Testing

Traditional software testing methods focus on verifying code behavior in specific, predefined scenarios. These methods include:

• Unit tests: These tests check individual components or “units” of code for correctness, ensuring each part works in isolation.

• Integration tests: These verify that all system components work together correctly.

• System tests: These cover end-to-end testing to ensure the entire system operates as expected.

• Runtime assertions: These checks are performed during execution to verify that certain conditions hold while the program runs.

• Fuzzing: An automated testing technique that inputs invalid, unexpected, or random data into a system. It’s effective at finding edge cases and vulnerabilities that conventional tests might miss.

While these testing methods are useful, they come with notable drawbacks:

• Limited scope: Traditional tests only validate specific cases or executed paths. They don’t cover all possible states the system could enter.

• Missed edge cases: Rare and unexpected combinations of inputs or system states can often go untested, leading to hidden bugs or potential system failures.

As a real-world analogy: Testing a ship only in calm waters doesn’t guarantee its performance in a storm. Similarly, code that passes all predefined tests may still fail in unpredictable, real-world scenarios.

Traditional test coverage tools provide metrics on the percentage of code covered by tests, but they don’t verify every possible state of the system**.** What we want is a more comprehensive solution that mathematically proves the legality of every state the system can enter, regardless of the specific test paths.

As Vitalik Buterin famously said, “Code is law” in the decentralized world. This means that any flaw in a smart contract is essentially a flaw in the system itself. By all means protocol developers must ensure that this “law” behaves as intended, catching potential bugs or vulnerabilities before they can be exploited.

The Case for Formal Verification

Here comes a more rigorous approach that operates and guarantees far beyond traditional testing:

• Exhaustive Validation: Instead of checking specific scenarios, formal methods ensure the system behaves correctly in every possible state.

• Proof of Security: It mathematically guarantees that the system won’t enter any illegal or unintended states — crucial for DeFi protocols handling billions in assets.

• No Missed Edge Cases: Every potential interaction is covered, leaving no room for untested vulnerabilities.

By moving from just “catching bugs” to proving correctness, formal verification aims to guarantee that smart contracts behave, even under complex conditions.

Formal Specifications

We need a way to define a system’s behavior as a clear set of rules to verify its correctness. This is where formal specifications come in, serving as the foundation for formal verification. These specifications define how the system should remain secure, predictable, and behave correctly under all possible conditions.

Below are key methods for defining formal specifications, with code examples in CVL:

Product Stories

Derived from user requirements and real-world usage scenarios.

Example: “User balance should always increase by the deposit amount after a successful deposit.”

rule depositIncreasesBalance(uint256 amount) {
     env e;     require(amount > 0);
     uint256 balanceBefore = balanceOf(e.msg.sender);
     deposit(amount);
     uint256 balanceAfter = balanceOf(e.msg.sender);
     assert(balanceAfter == balanceBefore + amount, "Balance did not increase correctly after deposit");
}

When writing formal verification rules, it’s helpful to follow this general structure:

1. Preconditions: Use require statements to set up the initial state and constraints.

2. Function Call: Execute the smart contract function being verified.

3. Postconditions: Use assert statements to check that the desired properties hold after the function executes.

This structure helps in clearly defining what conditions should be true before and after a function’s execution, making specifications more readable and maintainable.

Note: In CVL (Certora Verification Language), require and assert statements behave differently from their Solidity counterparts:

• A require statement that isn't met doesn't halt execution; instead, it filters out scenarios that don't meet the precondition.

• An assert a statement that isn't met results in a violation message and a backtrace, indicating a potential issue in the contract logic.

System Invariants

Invariants are properties that must always hold true throughout the system’s lifecycle.

Example: “The total supply of tokens remains constant unless explicitly minted or burned.”

invariant totalSupplyEqualsSumOfBalances() {
     totalSupply() == sum(address a in accounts, balanceOf(a));
}

Security Properties

These rules ensure that only authorized users can perform specific actions.

Example: “Only the contract owner can perform administrative actions.”

rule onlyOwnerCanPerformAdminActions() {
     env e;
     require(e.msg.sender != owner());
     performAdminAction@withrevert(e);
     assert(lastReverted, "Non-owner was able to perform an admin action"); 
}

This rule uses two important CVL-specific constructs:

• @withrevert operator indicates the function call might revert. The rule attempts to perform an admin action with a non-owner caller, allowing for the possibility of reversion.

• lastReverted keyword returns true if the previous operation reverted. The rule asserts that the action indeed reverted, confirming that non-owners cannot perform it.

This approach leverages CVL’s features to verify security properties by attempting potentially invalid operations and ensuring they fail as expected.

Protocol Behavior

Understanding the expected behavior of a protocol ensures that core functions operate correctly.

Example: “A user’s balance should decrease by the withdrawal amount.”

rule withdrawalDecreasesBalance(uint256 amount) {
     env e;
     require(amount > 0);
     uint256 balanceBefore = balanceOf(e.msg.sender);
     withdraw(amount);
     uint256 balanceAfter = balanceOf(e.msg.sender);
     assert(balanceAfter == balanceBefore - amount, "Balance did not decrease correctly after withdrawal"); 
}

General Guidelines for Rule Creation

Beyond these specific types, there are general guidelines for creating effective verification rules. These guidelines often derive from the nature of the system state or behavior being checked:

• Additivity: Verify that the sum of components equals the whole. For example, check if the total supply of tokens always matches the sum of all account balances.

• Monotonicity: Confirm that certain values change in only one direction under specific conditions. For instance, ensure a liquidity pool’s total value locked (TVL) only decreases during withdrawals and only increases during deposits.

• Bounds checking: Set and verify acceptable ranges for critical values. For instance, confirm that a token’s transfer amount never exceeds the sender’s balance.

• Composability: Ensure interactions between different protocols or contract modules don’t lead to unexpected states. For example, verify that a flash loan taken from one protocol doesn’t leave another integrated protocol in an inconsistent state after the transaction completes.

• Atomicity: Verify that multi-step operations either complete fully or revert entirely. For instance, ensure that in a token swap, either both token transfers occur or neither does.

By incorporating these principles, you can create a more comprehensive set of verification rules that cover complex interactions and edge cases in your smart contracts.

Symbolic Variables

In formal verification, symbolic variables represent entire ranges of possible values, allowing the verification system to evaluate whether rules hold for all potential states of the system.

For instance, when verifying a deposit() function, we might use a symbolic variable for the deposit amount. This single variable doesn’t represent just one specific amount, but rather any possible uint256 value greater than zero. The verification system can then reason about the behavior of the function for all valid deposit amounts simultaneously.

Similarly, we might treat the sender address as a symbolic variable, representing any valid Ethereum address. This allows the verification process to consider all possible user interactions with our contract.

This approach enables formal verification tools to:

1. Consider all possible inputs without explicitly testing each one.

2. Prove properties that hold for entire classes of inputs.

3. Discover edge cases that might be missed by traditional testing with concrete values.

In our upcoming practical example, we’ll see how these symbolic variables are used in formal specifications and how they enable comprehensive verification of smart contract behavior.

Practical Example: From Code to Proofs

Let’s consider a basic Vault contract where users can deposit and withdraw Ether:

contract Vault {
    mapping(address => uint256) public balances;
    function deposit() external payable {
        require(msg.value > 0, "Deposit must be greater than zero");
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(amount > 0, "Withdrawal amount must be greater than zero");
        require(amount <= balances[msg.sender], "Insufficient balance");
        balances[msg.sender] -= amount;
        payable(msg.sender).transfer(amount);
    }
}

Step 1: Defining Formal Specifications

We want to verify that a withdrawal always decreases the user’s balance by the exact amount withdrawn:

rule withdrawalDecreaseBalance(uint256 amount) {
    env e;
    require(amount > 0);
    require(amount <= balances[e.msg.sender]);
    
    uint256 balanceBefore = balances[e.msg.sender];
    withdraw(amount);
    uint256 balanceAfter = balances[e.msg.sender];
    
    assert(balanceAfter == balanceBefore - amount, "Balance not decreased correctly");
}

Step 2: Translating to Logical Formulas

The verification tool translates our specifications and relevant contract codes into logical formulas. These directly correspond to the components of our rule:

• Let A represent: amount > 0

• Let B represent: amount <= balances[e.msg.sender]

• Let C represent: balanceAfter == balanceBefore — amount

Step 3: Constructing the SAT Formula

These logical formulas are combined into a Boolean SAT (satisfiability) formula:

(A ∧ B) → C

In propositional logic, this translates to:

¬A ∨ ¬B ∨ C

Where: ¬ means not, ∨ means or, ∧ means and (though not used in this specific formula). This notation, known as a clause in Conjunctive Normal Form (CNF), is a standard format that SMT solvers use to process logical statements efficiently.

Therefore, the above formula simply reads: “Either the amount is not valid (¬A ∨ ¬B), or the balance is correctly decreased after withdrawal C”

We use the negation of the original formula because we’re employing a proof-by-contradiction approach. We’re asking the SMT solver to find a case where our assertion doesn’t hold. Therefore, the SMT solver searches for counterexamples to disprove our assertion. If no such is found, the system is proven correct.

Step 4: SMT Solving

The SAT formula ¬A ∨ ¬B ∨ C is passed to an SMT (Satisfiability Modulo Theories) solver. SMT solvers are powerful tools that determine whether a logical formula can be satisfied under certain constraints. Some popular SMT solvers include:

• Z3: Developed by Microsoft Research, widely used in formal verification

• CVC4: Developed by Stanford University, NYU, and the University of Iowa

• Yices: Developed by SRI InternationalZ3: Developed by Microsoft Research, widely used in formal verification

These solvers use sophisticated algorithms and heuristics to efficiently search the solution space, considering various strategies to quickly find potential violations or prove that no violations exist.

In our case, the SMT solver attempts to find an assignment that makes the SAT formula false, which would indicate a violation of our specified behavior.

Step 5: SMT Solver Results

The SMT solver tries to find an assignment of boolean values to our logical variables A, B, and C that makes the formula ¬A ∨ ¬B ∨ C false.

The reason we look at the negation is rooted in how we’re using formal verification to prove correctness. We’re trying to prove that our original formula (A ∧ B) → C always holds true. In other words, we’re asserting that there are no cases where A and B are true, but C is false.

To prove this, we use a proof-by-contradiction approach:

1. We assume there might be a case where our assertion doesn’t hold.

2. This case would be represented by A ∧ B ∧ ¬C (our preconditions are met, but our postcondition isn’t).

3. We ask the SMT solver to find such a case.

4. If the solver can’t find any such case, we’ve proved our original assertion.

The SMT proceeds to find an assignment that makes A ∧ B ∧ ¬C true. Let’s say it finds that assignment A = true, B = true, C = falsefalsifies the formula, indicating a potential violation of our specified behavior.

Step 6: Backtracking to a Counterexample

Now we need to interpret this abstract result in terms of our original specification and code. Here’s how we backtrack:

1. A = true means amount > 0

2. B = true means amount <= balances[e.msg.sender]

3. C = false means balanceAfter != balanceBefore — amount

This process of deriving concrete values from the abstract assignment is known as counterexample generation. It’s typically performed by the verification tool in conjunction with the SMT solver, using the theories understood by the solver (like integer arithmetic) to find specific values that satisfy the abstract conditions.

The SMT solver finds one possible set of values:

• amount = 100

• before withdraw: balances[e.msg.sender] = 100

• after withdraw: balances[e.msg.sender] = 1

This counterexample satisfies A and B (as they’re both true), and violates C (as it’s false).

Step 7: Tracing Back to Code

Interpreting this counterexample, we can see that our contract fails to correctly update the balance when a user withdraws their entire balance. The balance is decreased, but not by the exact amount withdrawn.

Step 8: Fixing and Re-verifying

To fix this issue, we need to ensure that the balance is decreased by exactly the withdrawal amount:

function withdraw(uint256 amount) external {
    require(amount > 0, "Withdrawal amount must be greater than zero");
    require(amount <= balances[msg.sender], "Insufficient balance");
    balances[msg.sender] -= amount;  // This line ensures the balance is decreased by exactly 'amount'
    payable(msg.sender).transfer(amount);
}

After making this change, we would run our formal verification again. If the SMT solver can’t find any assignment that falsifies our formula, we have mathematically proven that our withdrawal function correctly updates the balance for all possible valid inputs.

Verification Process Summary

This process — from code to logical formulas to SMT solving, and back to concrete scenarios — allows us to verify the correctness of our smart contracts with a level of certainty far beyond what traditional testing can provide:

By considering all possible states and transitions, formal verification helps us catch subtle bugs and edge cases that might otherwise go unnoticed, providing a powerful tool in our quest for secure and reliable smart contracts.

Certora Prover: Comprehensive Formal Verification

While we’ve explored how SMT solvers work in formal verification, let’s now explore a powerful tool that automates, streamlines, and enhances this process. Certora Prover, developed by a team of leading Ph.D. researchers in the field, is a scientific-heavy tool that pushes the boundaries of formal verification for smart contracts.

Certora Prover offers a wide range of features to enhance the verification process:

• Expressive Specification Language (CVL): Allows precise property definitions tailored for smart contracts.

• Automated Verification: Converts specifications and bytecode into SMT problems.

• Bytecode-Level Analysis: Provides more accurate and trustworthy verification results compared to source code analysis alone, as it accounts for any changes or optimizations introduced during the compilation process.

• Parameterized Systems: Allows verification of contracts that interact with other contracts, considering various possible implementations.

• Prover Debugger: Helps developers understand and debug the verification process itself.

• Rule-Code Coverage: Helps developers understand which parts of their code are covered by the verification rules, ensuring comprehensive testing.

• Mutation Testing: Automatically introduces small changes in the code to test the robustness of the verification rules.

• Detailed Feedback: Provides counterexamples for debugging when violations are found.

• Integration Capabilities: Works seamlessly with development tools and CI/CD pipeline.

The Challenges of Formal Verification

It’s important to note that formal verification is only as good as the specifications it tests against. If the specs don’t capture all edge cases or reflect intended behavior correctly, the verified code might still have problems. As they say, “Garbage in, garbage out.”

Computationally, the process of iterating through all possible states of a system is an incredibly complex problem. To put it simply, the number of possible states grows beyond exponentially with the complexity of the system. In computer science terms, this is known as an NP-hard problem or, in some cases, even an undecidable problem.

Because of this inherent complexity, a significant amount of scientific research goes into developing efficient heuristics. These heuristics aim to reduce the problem space by efficiently pruning irrelevant execution paths.

The goal is to minimize what is called “timeouts” — instances where the verification process exceeds a predefined time limit and is automatically terminated.

Despite these challenges, tools like Certora Prover have made significant strides in making formal verification practical for complex smart contracts.

Applicability of Formal Verification in Smart Contracts

Formal verification is particularly well-suited for smart contract verification due to several factors:

1. Single-threaded Execution: Smart contracts typically execute in a single-threaded environment, simplifying the verification process.

2. Relatively Short Code: Most smart contracts are concise, making them more manageable for exhaustive verification.

3. High-stakes Operations: With millions of dollars at stake, the cost of formal verification is justified by the potential losses it can prevent.

4. Immutability: Once deployed, smart contracts can’t be easily updated, making it crucial to verify correctness before deployment.

These characteristics make formal verification a powerful tool for enhancing smart contract security and reliability, especially for high-value DeFi protocols.

The Interconnected Nature of Security Measures

While formal verification is powerful, it’s most effective when used as part of a comprehensive security strategy. The most robust approach involves:

1. Continuous Verification: Every proposed change (e.g. pull requests submitted as a part of governance in AAVE protocol), including those through governance, should pass through a comprehensive security process, including formal verification, manual audits, automated analysis, and economic simulations.

2. Manual Audits: Expert reviewers manually inspect the code to identify issues that automated tools might miss, especially those related to business logic or novel attack vectors.

3. Real-Time Monitoring: Tools like Hypernative offer continuous blockchain state monitoring, which adds an additional layer of security to complement formal verification. These tools analyze transactions and system state changes in real-time, potentially catching harmful transactions and method calls before execution.

The Importance of Reputable Verification

Not all security audits are created equal. As users and investors in the DeFi space, it’s essential to evaluate the security measures of protocols you interact with. When assessing a protocol’s security:

Look for Reputable Verifiers: Seek out protocols that have been verified by well-respected firms known for their rigorous processes.

1. Multiple Audits: Protocols that have undergone multiple audits from different reputable firms often demonstrate a stronger commitment to security.

2. Ongoing Verification: Look for protocols that employ continuous verification processes, not just one-time audits.

3. Transparency: Check if the protocol makes its audit reports and verification results publicly available.

For a comprehensive history of smart contract exploits, resources like DeFi Llama’s “Rekt Database” (https://defillama.com/hacks) provide valuable insights into past vulnerabilities and their impacts.

Conclusion

The security of smart contracts and DeFi protocols presents a multi-faceted challenge that demands a comprehensive approach. By combining formal verification, rigorous manual auditing, continuous monitoring, and real-time analysis, we can create a robust security ecosystem. However, it’s important to understand that no single method, including formal verification, is perfect. The exponential complexity of verifying all possible states means that even the most advanced tools have limitations.

For users and investors in the DeFi space, understanding these security measures is crucial. Always look for protocols that employ a diverse range of reputable security measures and maintain transparency about their security processes. Remember, a protocol that undergoes continuous verification, including for all governance-proposed changes, demonstrates a stronger commitment to security than one that allows unaudited modifications.

As the field of formal verification continues to advance, driven by cutting-edge research and practical applications in high-stakes environments like DeFi, we can expect even more sophisticated tools and methodologies to emerge. This ongoing evolution of security practices will play a vital role in building a more secure and trustworthy decentralized future.

Resources

For readers interested in deepening their understanding of formal verification and the Certora Prover, here is a curated list of valuable resources I’ve found particularly helpful:

• The comprehensive CVL tutorial with explanations: https://docs.certora.com/projects/tutorials/en/latest/

• Code-based tutorial with a set of runnable examples: https://github.com/Certora/Tutorials/

• A nice introduction to Certora Prover: https://www.youtube.com/watch?v=jv_1hEeG-lk&t=1849s&ab_channel=Certora​ by Mike George from Certora

• Certora Prover walkthrough: https://www.youtube.com/watch?v=c5ViO3Dpfqs&ab_channel=Certora​ by Chandrakana Nandi from Certora

• Checking formal specifications workshop: https://www.youtube.com/watch?v=PjUua2Hi1GA&t=1568s&ab_channel=Certora​ by Nurit Dor from Certora

• Certora Discord is the best place to get help on every question along the road from onboarding to heavy usage: https://discord.gg/certora (with special thanks to Aleksander for his patience in answering all my questions and for reviewing this article)

Find me on LinkedIn, Telegram, X (a.k.a. Twitter), Farcast.

Retrospective / Preface

The DeFi landscape has evolved significantly since the yield farming frenzy of 2020–2021. While those days were characterized by unsustainable triple-digit APYs and subsequent market crashes, today’s yield mechanisms are more sophisticated and diverse. Pendle emerges in this new era, offering innovative solutions for yield management that address the lessons learned from past experiences.

Yield-Generating Assets

To understand Pendle’s innovative approach, we first need to explore the foundation of its ecosystem: yield-generating assets.

Every asset that provides additional perks while owned is defined as a yield-generating (or yield-bearing) asset. Sometimes, protocol holders can earn additional perks by performing specific actions like locking more tokens at specific times, sharing their email, joining a Discord server, inviting friends, or just clicking on icons for a few days in a row.

During the previous era of staking, the decision on which asset to stake mainly involved three factors:

• The APR/APY

• The actual asset price

• The code quality and audits (since many staking smart contracts were exploited, leading to losses)

Nowadays, yield comes in various forms. Examples include:

• stETH: Staking ETH in Lido generates approximately 3% annual growth.

• DAI: Staking in Compound yields around 5.5% in DAI and 1% in COMP annually.

• ETH: Restaking in Ether.Fi offers various perks like ETH, ETHFI tokens, EigenLayer points, AVS rewards, and Ether.Fi points, with new game rules frequently introduced. Simple actions like daily check-ins can earn more points and multipliers.

Yield Tokenization

With a clear understanding of yield-generating assets, we can now delve into how Pendle revolutionizes its management through yield tokenization.

The main idea behind yield tokenization is to separate the original asset (a.k.a. principal asset, the one being staked or locked) from its yield (generated by the locking protocol). This approach introduces new capital management strategies, especially in bullish market conditions and in the context of the EigenLayer ecosystem. If EigenLayer does not sound too familiar read my article here. It covers in-depth the protocol mechanics with diagrams and representative usage scenarios.

Yield-representing tokens are priced significantly lower than the original asset because they represent only the market’s expectation regarding the future yield of the underlying protocol, not the actual asset value. Therefore, if the market expects the yield to stay above 5%, the yield token price might be around 5% (or higher, depending on market expectations) of the original asset’s price. This allows investors to gain exposure to yield potential with less capital.

Example: Suppose you expect the APY on a specific asset (e.g., DAI) to increase from 5% to 10%. Instead of buying more DAI, you can buy yield-representing tokens, which are much cheaper. If the market expectation is 5% of the underlying asset, the yield token price will be around 100%/5% = 20 times cheaper than the asset price. This roughly equates to 20x leverage trading of the original asset.

Pendle Tokenization Mechanism

Let’s examine the core of Pendle’s innovation: its unique tokenization mechanism that separates yield from principal. We’ll start with the two main use cases insightfully identified by Pendle.

Alice, the Conservative Institutional Investor

Alice hopes that the principal stable token (USDe) will not de-peg keeping its price until maturity. Alice prefers a guaranteed return, protecting her investments from yield volatility. In Pendle terms, Alice buys a PT (Principal Token), so that:

• Represents the right to redeem the full principal at maturity. The token is initially sold at a discount. Therefore, the yield upon maturity is guaranteed by code when the token reaches its original price.

• The PT token is tradeable at all times vs the principal token so that if USDe drops or raises dramatically in price, Alice can abandon her PT token or take the revenue ahead of time.

Example: Alice buys 100 PT-USDe at $94.5, and receives $100 at PT maturity.

Bob, the Degen Yield Optimizer

Bob has just discovered the EigenLayer ecosystem and is bullish on the potential to boost rewards from Renzo Protocol, EigenLayer, and Actively Validated Services (AVSs) altogether. Bob buys YT-ezETH tokens to maximize his exposure to these potential yield increases.

• The token allows Bob to receive all the actual yield generated by staked ETH until maturity, starting from the time of purchase.

• While PT holders enjoy a guaranteed interest upon maturity, YT holders like Bob can claim the accrued staking rewards in real time, thanks to the integration with the underlying ezETH protocol.

• The YT token is tradeable, allowing Bob to speculate on yield expectations. However, the YT value typically decreases over time and goes to zero upon PT maturity.

Example:

Initial conditions:

• 1 ezETH is worth $3,500

• The expected APY is 5%

• Token maturity: 1 year

Step 1: Bob buys YT-ezETH for 1 ezETH

• Expected yield for 1 year: 5% of $3,500 = $175

• YT-ezETH price for 1 ezETH: $175

• Bob buys YT-ezETH for the worth of 1 ezETH, exposing his investment to x20 leverage factor: $3,500 / $175 = 20x

Step 2: APY jumps to 20%

• New expected yield for 1 year: 20% of $3,500 = $700

• New theoretical YT-ezETH price: $700

Step 3: YT price reaction

• Let’s assume the YT-ezETH price doesn’t fully reflect the new yield immediately

• New YT-ezETH price: $500 (reflecting increased yield expectations but with some lag)

Step 4: Bob’s position

• Initial investment: $175

• Current YT-ezETH value: $500

• Unrealized profit: $500 — $175 = $325

• Return on investment: ($325 / $175) * 100 = 185.7% in addition to all EigenLayer and Renzo Protocol rewards such as AVSs points, REZ token, and EigenLayer points.

Biting the “Zero-Sum” Game

Every market needs a zero-sum game, enabled by pairs of assets that balance each other against a well-defined invariant. Pendle documentation refers to the formula:

PT + YT = Underlying asset price

The principal price is incorporated in the Principal Tokens (PTs), while the yield aspect is revealed in both Principal Tokens (PTs) and Yield Tokens (YTs).

Let’s explore the initial discount on the PT, which enables a guaranteed revenue upon maturity. That “bite” from the actual PT price at the market launch time, becomes the initial price of the YT, enabling the yield-generating token.

Example: with a 100 DAI asset yielding 6% annually and 1-year maturity:

• PT might be priced at 94.5 DAI

• YT would be initially priced at 5.5 DAI

The initial ‘bite’ or discount is crucial to Pendle’s mechanism. Thanks to the talks in the Pendle discord, I’ve learned that it’s calculated based on current market conditions and historical data. Specifically, the smart contract looks at:

• Past market consensus of implied yield from previous pools, if available.

• The last 7-day average underlying yield as an alternative. This approach ensures the initial pricing reflects both market expectations and recent yield performance, creating a fair starting point for both PT and YT holders.

Keeping the Equilibrium

Understanding the zero-sum nature of Pendle’s system, we can now explore how this equilibrium is maintained in practice. Let’s explain how the market stays efficient based on the arbitrage use case:

Charlie, the Arbitrageur

• Observes: PT at 0.93 DAI, YT at 0.06 DAI. Action: Spends 1 DAI to buy 1 PT and 1 YT.

• At maturity: PT redeems for 1 DAI, YT yields additional profit (let’s say 0.04 DAI)

• Total return: 1 DAI (from PT) + 0.04 DAI (from YT) = 1.04 DAI

• Profit: 1.04 DAI — 1 DAI initial investment = 0.04 DAI

This risk-free profit incentivizes arbitrageurs to maintain the PT + YT = Underlying asset price equilibrium.

Pendle’s AMM Structure

Pendle’s innovative tokenization wouldn’t be complete without a robust trading mechanism. This is where Pendle’s unique AMM structure comes into play. The key components of this structure are:

• A single liquidity pool type: PT/SY (Principal Token / Standardized Yield)

• Support for both PT vs Principal and YT vs Principal trades (YT vs Principal trades are enabled via a flash swap mechanism using the same PT/SY pool)

SY (Standardized Yield) is a token standard (EIP-5115) developed by the Pendle team that:

• Wraps any yield-bearing token

• Provides a standardized interface for interacting with various yield-generating mechanisms

• Acts as a building block for future DeFi applications

• Is a purely technical component, e.g. users don’t interact with it directly

This structure offers several advantages:

• Efficient Price Discovery: The PT/SY pool allows for an intuitive valuation of both PT and YT against the standardized yield-bearing asset.

• Liquidity Optimization: Using a single pool type (PT/SY) allows for more efficient utilization of liquidity.

• Capital Efficiency: Liquidity Providers (LPs) earn fees from both PT and YT swaps from a single liquidity provision.

It’s important to note that while PT + YT = Underlying asset value maintains as an equilibrium, the individual prices of PT and YT are subject to market forces. At maturity, PT will always be redeemed 1:1 to the underlying asset, while YT decays to 0.

Pendle’s AMM design also significantly mitigates the risk of impermanent loss (IL) for liquidity providers. Unlike traditional AMMs where IL can be substantial due to price divergence between paired assets, Pendle’s system ensures that PT generally follows the price of the original asset (wrapped as SY) closely, becoming 1:1 at maturity. This design feature makes liquidity provision in Pendle’s AMM a more predictable and potentially profitable endeavor, with negligible IL risk.

By combining efficient trading mechanisms, optimized liquidity utilization, and minimal impermanent loss, Pendle’s AMM structure offers a robust and attractive platform for both traders and liquidity providers.

Lifecycle of a Pendle Token

To truly grasp how all these components work together, I have tried to play with the numbers creating a set of examples with a hypothetical yield-bearing asset called yUSD, which represents a yield-bearing USD stablecoin. We’ll examine its behavior over 1 year with the following initial conditions:

• Underlying yUSD price: $100

• Expected annual yield: 10%

• Maturity: 1 year from now

Sidenote: To avoid redundant zeros in our calculations, I am using $100 as the base price for yUSD instead of $1.

Let’s break this down into quarters:

The YT price typically decreases over time as the remaining yield potential diminishes, approaching zero at maturity. Conversely, the PT price increases, converging towards the full principal amount at maturity. This reflects the changing time value and risk profile of each token as the maturity date approaches.

Now, let’s examine some edge cases:

Edge Case 1: Unexpected Yield Increase

This scenario demonstrates how Pendle’s system adapts to sudden changes in yield expectations. When the expected yield doubles at Day 180, the system adapts through market forces and arbitrage:

• Initial state (Day 90): PT = $97.50, YT = $5.00, Total = $102.50

• Yield expectation doubles (Day 180):

• YT price should increase to reflect higher future yield

• PT price should decrease as more value is attributed to yield

• Market reaction: YT price jumps to $8.75, PT drops to $96.25, Total = $105.00

Arbitrage mechanism: If the market overreacts, creating a mismatch (e.g., YT = $9.00, PT = $96.25, Total = $105.25):

• Arbitrageurs sell 1 YT for $9.00

• They buy 1 underlying yUSD for $100

• They split this yUSD into 1 PT and 1 YT

• They sell the newly created PT for $96.25

• Net profit: $9.00 + $96.25 — $100 = $5.25 (minus fees and slippage)

This process continues until PT + YT = yUSD ($100). This arbitrage ensures the system maintains equilibrium despite the shock in yield expectations.

This scenario demonstrates Pendle’s ability to adapt to sudden yield changes while maintaining overall equilibrium through market forces and arbitrage.

Edge Case 2: Underlying Asset Value Decrease

When yUSD drops 10% at Day 180, PT and YT prices adjust to maintain the equilibrium.

This adjustment maintains the equilibrium PT + YT = yUSD price in the face of underlying asset volatility, demonstrating Pendle’s resilience to significant market movements while preserving the yield tokenization structure.

This case illustrates Pendle’s resilience to underlying asset volatility, showing how the system adjusts to maintain the fundamental PT + YT relationship.

Edge Case 3: High Yield Uncertainty Near Maturity

This scenario showcases the impact of yield uncertainty as the token approaches maturity:

• Initial expectation: 10% annual yield

• Actual yield by Day 365: 12% (higher than expected)

What happens:

• YT price becomes more volatile due to uncertainty (e.g., fluctuating between $7.50 and $8.75)

• PT price remains relatively stable, approaching $100 (full principal)

YT price volatility increases near maturity because:

• Less time for yield generation means each yield change has a larger relative impact

• Market participants have differing short-term yield expectations

• Any new information about potential yield has a more immediate effect

User benefit:

• Initial YT price (Day 0): $5.00 (expecting 10% yield)

• Final yield payout: $12.00 (12% of $100)

YT holders benefit because they receive the actual yield, which exceeds expectations. They paid for an expected 10% yield but received a 12% yield, resulting in a 20% higher return on their investment (($12 — $10) / $10 = 20% increase).

This example highlights how Pendle handles yield uncertainty near maturity, benefiting YT holders when yields exceed expectations while maintaining PT stability.

Risks and Limitations

As with any complex financial system, Pendle comes with its own set of challenges. Let’s examine the potential risks and limitations users should be aware of:

• Smart Contract Risk: Despite rigorous audits, Pendle’s smart contracts may contain unforeseen vulnerabilities. For example, a bug in the yield calculation mechanism could lead to incorrect token pricing. Pendle mitigates this through regular audits and bug bounty programs.

• Market Volatility: Extreme market conditions could cause significant price discrepancies between PT, YT, and the underlying asset. A sudden drop in ETH price, for instance, could lead to unexpected losses for YT holders. Users can hedge their positions by combining PT and YT from different assets.

• Liquidity Risk: During periods of low liquidity, users might struggle to enter or exit positions at desired prices. This could be particularly problematic near maturity dates when many users may want to close positions simultaneously. Pendle incentivizes liquidity provision to maintain deep pools.

• Complexity: The system’s sophistication might confuse less experienced users. For example, a user might inadvertently sell their YT, thinking they’re only trading excess yield, and miss out on future yield appreciation.

• Regulatory Uncertainty: Evolving DeFi regulations could impact Pendle’s operations or token classifications. Securities regulators might, for instance, classify YTs as derivatives, potentially limiting their accessibility.

• Underlying Asset Risk: Issues with yield-generating assets could affect both PT and YT values. A de-pegging event in a stablecoin used as an underlying asset would impact all associated Pendle tokens.

• Oracle Dependence: Accurate pricing and yield calculations rely on oracles, which could be manipulated or fail. An oracle reporting inflated yield data could lead to mispricing of YTs.

• Maturity Mismatch: Users must be aware of token maturity dates to avoid unexpected value changes or expirations. Holding a YT past its maturity date, for example, would result in holding a worthless token.

Composability

Despite these challenges, Pendle’s design opens up a world of possibilities through its high degree of composability with other DeFi protocols. By separating principal and yield into tradable tokens, Pendle offers versatile building blocks for complex financial strategies:

• Collateralized Borrowing: Use PTs as collateral on lending platforms like Aave to borrow stablecoins, while retaining YTs for yield exposure. This allows users to leverage their principal while still benefiting from yield appreciation. Example: Alice deposits 100 DAI PT on Aave, borrows 70 USDC, and uses it to buy more YT, amplifying her yield exposure.

• Cross-chain Yield Strategies: Bridge Ethereum-based PTs to other networks like Polygon or Arbitrum, using them in those ecosystems’ DeFi protocols. This enables users to capitalize on yield opportunities across multiple chains. Example: Bob bridges 100 USDT PT from Ethereum to Polygon, and uses it as collateral in a Polygon DeFi protocol, earning additional yield.

• Yield Tranching: Combine high-yield, high-risk YTs (e.g., from newer, more volatile protocols) with low-yield, low-risk PTs from established assets. This creates customized risk-return profiles catering to different investor appetites.

• Options on Yield: Develop option contracts on ETH staking YTs, allowing users to speculate on or hedge against future changes in staking rewards. This adds a new dimension to yield management and risk mitigation.

• Yield-boosted Savings Accounts: Create stablecoin savings products backed by DAI PTs, using YTs to boost the offered APY. This provides users with stable principal protection while offering competitive yields.

These examples showcase how Pendle’s tokenized yield becomes a versatile component in the DeFi ecosystem, enabling innovative financial products and strategies previously unattainable in traditional finance or early DeFi systems.

Future Developments

With a solid understanding of Pendle’s current mechanics and potential, let’s look ahead to the exciting developments on the horizon. Pendle continues to evolve with the upcoming Pendle V3, set to launch in 2024. This new version promises the following significant advancements:

Native Cross-margin Engine

• Allows users to manage multiple positions across different assets and maturities within a single margin account.

• Reduces capital inefficiencies by netting out positions and sharing collateral across trades.

Example: A user can now use their ETH-based PT as collateral for trading USDC-based YTs without needing separate deposits.

The native cross-margin engine could allow users to more efficiently leverage their positions across multiple assets, potentially increasing overall capital efficiency in the Pendle ecosystem.

• Introduces a new order type where users specify their desired outcome rather than exact execution parameters.

• The system automatically finds the best execution path, potentially across multiple liquidity pools.

Example: Instead of placing a specific swap order, users can input “I want to maximize my YT exposure for 1000 USDC,” and the system will determine the optimal execution across available markets.

These innovative developments offer more sophisticated, efficient, and flexible tools for yield management and trading.

The intents-based execution might lead to more complex yield optimization strategies, as users can more easily express complex trading goals.

The native cross-margin engine could allow users to more efficiently leverage their positions across multiple assets, potentially increasing overall capital efficiency in the Pendle ecosystem. The intents-based execution might lead to more complex yield optimization strategies, as users can more easily express complex trading goals.

Conclusion

• In this deep dive into Pendle’s mechanics, we’ve covered many concepts, from the basics of yield-generating assets to the intricacies of Pendle’s tokenization mechanism. We’ve explored how Pendle separates yield from the principal, creating a flexible system that caters to various investor needs — from conservative principal-seekers to yield optimizers and even yield shorters.

• Through detailed examples and edge cases, we’ve illustrated how Pendle maintains its core equilibrium of PT + YT = Underlying asset price across various market conditions. We’ve seen how the system handles unexpected yield increases, underlying asset volatility, and even extreme market optimism, showcasing the robustness of Pendle’s design.

• As DeFi continues to mature, protocols like Pendle demonstrate the sophisticated financial instruments that can be created on-chain. By tokenizing yield and creating liquid markets for future yield expectations, Pendle opens up new strategies for capital efficiency and risk management in the digital asset space.

Sources

• https://docs.pendle.finance/Home

• https://handbook.pendle.finance/

• https://app.pendle.finance/trade/education/learn

• https://pendle.gitbook.io/pendle-academy

• 
  
• 
  

Acknowledgments

It’s worth noting that the depth of understanding displayed in this article owes much to the Pendle community, particularly the knowledgeable members of the Pendle Discord. Unlike many crypto communities where discussions rarely venture beyond token prices and redemption processes, the Pendle community stands out for its technical depth and willingness to engage with complex protocol mechanics. Their insights and patience in explaining intricate details have been invaluable in crafting this comprehensive overview.

Find me on LinkedIn, Telegram, X (a.k.a. Twitter), Farcast.

In this guide, the examples provided will primarily utilize the EigenLayer ecosystem. However, the principles and strategies discussed are broadly applicable, making this article valuable for anyone interested in restaking, regardless of the specific platforms they use. Understanding these general patterns allows you to effectively apply them across various ecosystems and enhance your staking experience.

Understand the Overall Restaking Mechanics

Restaking involves staking Liquid Staking Tokens (LST) or Liquid Restaking Tokens (LRT). You can obtain LST/LRT in two primary ways:

• Stake ETH at a liquid restaking token (LRT) platform.

• Stake ETH at a liquid staking platform to receive a liquid staking token (LST) and restake it at an LRT platform.

Dare to Discover Multistep Investing Strategies

• Trade ETH (or other tokens) for LST/LRT on any decentralized exchange (DEX) and restake it at an LRT platform.

• Explore custom strategies on different platforms. For instance, Ether.Fi and its partners have created a special Liquid ETH Yield Vault that offers attractive bonus point multipliers when you deposit eETH, a liquid staking token you can acquire by staking ETH or trading for it.

The possibilities don’t end there. Once you have LST or LRT, you can:

• Restake them on another LRT platform like Renzo Protocol or Swell.

• Use as collateral on platforms like Zerolend.

• Trade them for other tokens on DEXes.

• Restake with leverage repeatedly combining the three above.

• Transfer them across bridges to other Layer 2 (L2) networks or the Ethereum Mainnet.

After restaking, you can earn various perks, such as:

• Coins (e.g., REZ from Renzo Protocol) that can be traded or converted to tokens at the end of an epoch.

• Points that might become tradable coins in the future. For example, staking on Ether.Fi can earn you EigenLayer points, Ether.Fi loyalty points, and 3%+ APY staking rewards.

Beyond restaking, you can earn rewards by:

• Borrowing against collateral.

• Providing liquidity to DEXes, also known as “liquidity mining”.

• Trading on DEXes; for instance, Hyperliquid previously rewarded traders with points based on trading volume.

Despite its potential, restaking comes with its quirks and challenges due to the early stage of the technology and user experience (UX). The following checklist aims to help you navigate these challenges and minimize unpleasant surprises.

Always Remember Your Way Back Home

When implementing a multi-step strategy, such as trading tokens, bridging them to another chain, and restaking them as collateral, it’s crucial to keep a clear record of your transactions. This ensures you have a plan to unlock your funds when needed. Utilize tools like Debank to track your transactions, but consider maintaining a personal spreadsheet for comprehensive records.

Evaluate Which Tokens Are Accepted and How to Get Them

Certain restaking protocols may require specific tokens as restaking deposits. For example, Ether.Fi accepts only wETH, eETH, and weETH (explained below). Ensure you understand how to acquire the necessary tokens for the protocols you are participating in. To avoid bridge fees, verify that these tokens are available (through restaking or trading) on the same Layer 2 blockchain where you intend to restake them.

Now, a few words on the aforementioned tokens:

• eETH (Ether.Fi ETH): Your “receipt” for staking ETH on ether.fi, representing your share of the growing staking rewards pool.

• wETH (Wrapped ETH): wrapped in an ERC-20 compatible format, allowing it to be used in Decentralized Finance (DeFi) applications such as decentralized exchanges (DEXes), lending platforms, and yield farming protocols. As the original ETH was created before the common standard used by these applications.

• weETH (Wrapped Ether.Fi ETH): eETH converted in the same way as ETH to wETH for the same purpose of using it within dApps.

Understand Campaign Details

Before participating in any restaking protocol, it’s essential to understand the campaign details, including:

• Epochs and Deadlines: Each protocol might have specific periods during which you can withdraw your staked assets without penalties or post-campaign periods when you can claim rewards. Familiarize yourself with these timelines to avoid any unexpected fees or issues.

• Accepted Tokens: Verify which tokens are accepted as restaking deposits. For example, Ether.Fi accepts only wETH, eETH, and weETH.

Verify the Most Updated Information

To ensure a smooth restaking process, always verify that you have the most up-to-date information by checking the project’s official channels and documentation:

• Staking Conditions: Check conditions such as the cap for the epoch is filled. Once a cap is reached, additional staking might be restricted or yield lower rewards.

• Technology Glitches: Expect various glitches since the technology is in its early stages. For instance, restaking positions might not be immediately reflected in the user interface: On Ether.Fi, only Ethereum Mainnet restakes are currently displayed, not those on recently supported L2s like Linea.

• Page Refreshing and UX Considerations: Due to the evolving nature of these platforms, you might encounter outdated page information. Always refresh the page to ensure you have the latest details, like deposit caps. For instance, on Mitosis, a grayed-out multiplier indicated the deposit cap had been reached, even though the deposit button remained active. It’s crucial to pay attention to these visual cues for accurate information.

Evaluate the Supported L2 Layers

Different Layer 2 (L2) solutions may offer varying multipliers for points and rewards, impacting your staking returns. It’s important to:

• Check All L2 Chains: Verify which chains are supported. Moving tokens across L2 chains often involves bridges and associated fees unless you already have the tokens on that specific chain.

• Assess Multipliers: Evaluate the multipliers available on different L2 chains. For example, at Mitosis, restaking on Mainnet had a 1.1 multiplier, while other L2s had a 1.2 multiplier.

• Assess Available Services: When selecting an L2, prioritize those that offer essential services without requiring bridges. Look for a user-friendly DEX with sufficient liquidity and collateral borrowing options to enhance your restaking experience.

Optimal Acquisition of Liquid Restaking Tokens (LRT)

Determine the most cost-effective method to acquire Liquid Restaking Tokens (LRT):

• Direct Staking: Compare the benefits of staking ETH directly to obtain LRT.

• Exchanging ETH: Evaluate the option of exchanging ETH for wrapped versions that might be more suitable for restaking.

Check Bridges and Transaction Fees

When dealing with cross-chain transactions, it’s essential to:

• Evaluate Bridges: Check the bridges used for cross-chain transactions.

• Assess Fees: Evaluate the associated transaction fees. Lower fees can maximize your net rewards.

Community Management and Responsiveness

If the details mentioned above have left you feeling confused, a good guiding hand can make a significant difference. An active and responsive community is crucial for navigating the complexities of restaking. Here’s what to look for:

• Join Project Channels: Join and monitor the project’s Discord or other community channels. These platforms often provide real-time updates and answers to your questions. Joining these communities may involve connecting your wallet and completing a verification process to ensure authenticity.

• Evaluate Responsiveness: Gauge the responsiveness and activity level of the community management. A responsive team can help clarify doubts, provide support, and ensure you stay informed about any changes or updates.

• Look for Community Engagement: Active community discussions and engagement can be a sign of a healthy and supportive ecosystem. Engaged users often share valuable insights and tips that can enhance your restaking experience.

Stay Updated on Protocol Changes

To adapt quickly to new rules or opportunities, staying updated on protocol changes is crucial:

• Stay Connected on Social Media: Follow the platforms you’re engaged with on Twitter and Discord, particularly their official announcement channels, to receive timely updates and notifications.

• Check for Updates Regularly: Regularly check for updates or changes in the protocols you’re staking with. This ensures you can adapt to new rules or opportunities quickly.

Diversify Your Staking Portfolio

To mitigate risks and increase potential returns, diversifying your staking portfolio is essential. Here’s how you can do it:

• Spread Assets Across Protocols: Distribute your staked assets across multiple protocols to reduce risk. By not putting all your assets in one protocol, you can minimize potential losses if one protocol experiences issues.

• Explore New Opportunities: Stay informed about new restaking opportunities, as new platforms and chains often emerge. Diversifying across different platforms and chains can help maximize your returns.

Understand Risks

Being aware of the risks associated with restaking is crucial to avoid unexpected losses. Here are some key points to consider:

• Audit and Slashing Risks: Understand the risks such as auditing by an unknown vendor and slashing conditions and penalties for the protocols you participate in. Slashing can occur due to various reasons, such as downtime or malicious activity, leading to a loss of staked assets.

• Early Stage Technology: The technology behind these projects is often in its early stages, therefore occasional glitches may occur. For example, your restaking positions might not be immediately reflected in the user interface, or you might see outdated information.

• Market and Liquidity Risks: Be mindful of market fluctuations and liquidity issues. Low liquidity can affect your ability to trade tokens efficiently and might result in unfavorable prices.

Conclusion

Restaking offers a valuable opportunity to maximize your rewards within the Ethereum ecosystem, but it comes with its own set of complexities and risks. By following this comprehensive checklist, you can navigate these challenges more effectively, make informed decisions, and optimize your staking strategy.

Remember, the key to successful restaking lies in careful planning, active engagement with the community, and continuous learning.

If you have any advice, corrections, or additional insights, please let me know in the comments. Happy (re)staking!

Addendum

If you’re new to EigenLayer and want to understand the basics of staking and restaking on this platform, read EigenLayer: A Beginner’s Guide to Enhancing Ethereum Rewards Through Staking and Restaking.

Find me on LinkedIn, Telegram, X (a.k.a. Twitter), Farcast.

If you’re already familiar with the basics of staking, feel free to skip the initial background sections to focus on the more detailed discussions of EigenLayer and restaking.

What Are Validators?

• When Alice wants to send 0.1 ETH to Bob, a validator checks to ensure Alice’s account has the necessary funds and that the transaction does not violate any network rules, such as attempting to spend the same ETH twice.

• Validators are crucial for maintaining the security and integrity of Ethereum’s Proof-of-Stake (PoS) system.

• To run a validator, one must stake 32 ETH as a financial commitment. This stake acts as collateral against any dishonest behavior, such as going offline or submitting incorrect or fraudulent transaction information.

• Validators are compensated for their work with rewards that include base fees and transaction fees. They may also earn additional income through more complex methods like MEV (Maximum Extractable Value), which are beyond the scope of this article.

Here is a diagram of Alice sending 0.1 ETH to Bob:

Why Run a Validator?

• Joe has staked 32 ETH to become a validator. This commitment allows him to earn rewards, typically between 3–5% annually (down ~2% from the last year), as compensation for helping secure the network.

• The staked 32 ETH are locked and remain inaccessible for the duration of their time securing the network. This means Joe cannot spend, invest, or use them for other purposes during this period.

• To operate a validator, it’s mandatory to stake a full 32 ETH. This not only contributes to the network’s security but also aligns the validator’s financial interests with the well-being of the entire Ethereum system.

This diagram shows how a Validator is set up:

Liquid Staking: Simplifying Ethereum Investment and Validator Management

For those with less than 32 ETH or without the technical know-how to manage an Ethereum Validator, options like liquid staking solutions are worth considering.

• Liquid staking platforms, such as Lido or RocketPool, have introduced two key features that users quickly adopted:          ◦ Individuals with ETH but lacking technical expertise can participate by investing any amount, not necessarily a full 32 ETH.          ◦ Tech-savvy operators can pool their resources within these platforms to run Ethereum Validators.

• The rewards from staking are shared between these investors and the technical participants.◦ For example, when Joe stakes ETH with RocketPool, he receives rETH, RocketPool’s liquid staking token, in return.

• These Liquid Staking Tokens (LST), such as stETH from Lido and rETH from RocketPool, are integrated into the DeFi ecosystem, offering flexibility such as being traded or used as collateral for loans.◦ For instance, Joe can exchange her rETH for USDT and use those funds to purchase other tokens.

• This innovation has made the originally illiquid 32 ETH stake more fluid, allowing more people to stake ETH across wider geographical regions and consequently boosting adoption and decentralization.

• Discussing tokenomics, governance, and comparisons of Liquid Staking platforms falls outside this article’s focus.

Here is a simplified diagram that illustrates how liquid staking platforms work (RocketPool is taken as a representative example):

Challenges in Ethereum Ecosystem Security

• With nearly $100B USD (32M ETH) staked by validators, Ethereum’s Layer 1 (L1) network is highly secure against 51% attacks. Such an attack would require acquiring an additional 32 million ETH, significantly increasing demand and driving ETH prices up, making the attack prohibitively expensive.

• The infrastructure of the Ethereum ecosystem, including Bridges, Oracles, Coprocessors, and Validators for Sidechains, is significantly more vulnerable to 51% attacks, which are considerably less expensive to execute compared to attacks on the main network.

• The infrastructure components of the Ethereum ecosystem, including bridges such as Omni Network, Wormhole, and Hyperlane along with oracles like Chainlink, API3, and Pyth, are more susceptible to 51% attacks, which generally cost less to execute compared to those targeting the main network.

Restaking and Multi-Protocol Security: A Look at EigenLayer

• Restaking extends the concept of liquid staking. Instead of backing just Ethereum validators with pooled ETH, it can back several systems, creating a stronger security net.

• A platform like EigenLayer allows restakers for the same ETH to be allocated to multiple validators operating across various protocols, making their investment work harder to gain a higher outcome potentially.

• In the regular investing world, there’s nothing quite like this. EigenLayer’s system is special because it lets stakers “double-dip” earnings from several protocols at once, using just a single investment.

• An important clarification: Staking with EigenLayer does not automatically grant each protocol the same level of security as Ethereum’s Layer 1, as this would expose every stake to extreme risk. Stakers first place their ETH/LST with EigenLayer, and then they must actively choose how much of their stake to delegate to various operators. The stake distribution is at the staker's discretion, impacting the level of security and potential rewards tied to the AVSs they select.

• Currently, each wallet can delegate to only one Operator; to distribute 1 ETH across multiple operators, multiple wallets are required. Furthermore, changing operators involves unstaking from EigenLayer, a process that takes seven days for LST and 24 days for EIGEN coins, after which staking must begin anew.

Joe’s Staking Choices

• Joe can first stake his ETH with a liquid staking service, such as Lido, RocketPool, and many others, receiving tokens that he can re-stake with an EigenLayer operator.

• If Joe runs his own Ethereum Validator he can delegate his Validator keys to EigenLayer, get the 32 ETH on his balance, start earning EigenLayer points, and be able to delegate these 32 ETHs to any EigenLayer Operator.

For Joe, if he wants a straightforward approach without managing staking and restaking processes, the simplest option is to use Liquid Restaking Token (LRT) platforms. Keep reading as more details on LRT platforms are provided in the dedicated section below.

EigenLayer Architecture: AVSs and Operators Explained

• Active Validator Systems (AVSs) are responsible for validating and securing a range of services, including bridges, oracles, coprocessors, data availability layers, and other blockchain-based applications, each focusing on distinct functionalities that enhance the capacity and capabilities of the network.

• Operators evaluate the risk and select which AVSs to run.

• Restakers like Joe can delegate their stakes to these Operators, who then restake the funds to the appropriate AVSs.

• Restakers like Joe can delegate their stakes to Operators, who then restake 100% of the received stake to each AVS selected by that Operator.

• Multiple operators can collaborate and support the same AVS, enhancing the system’s resilience.

• Questions like how operators distribute stakes among AVSs are part of the considerations Joe needs to make.

Examples of Active Validator Systems on EigenLayer: Enhancements and Roles

• EigenDA: It helps rollups on Ethereum to be more efficient by cheaper ordering and storage of transactions (trustless/cryptographical — check the docs).

• Brevis coChain AVS: Aims to make different blockchains work smoothly together, which is like making sure trains from different companies run on time on the same tracks.

• AltLayer MACH: Provides a way for separate blockchain systems to interact, similar to translators in a multi-language conference ensuring everyone understands each other.

• eoracle: Supplies trustworthy external data to blockchain networks, acting like a news reporter providing the latest updates for smart contracts to use.

• Omni Network: Works to connect Ethereum’s various layers quickly, reducing wait times much like a direct express elevator in a very tall building.

LRT (Liquid Restaking Token) Platforms

Remember Joe, who had to go through the hassle of staking ETH with Lido to receive stETH, which he then had to restake on EigenLayer? What if Joe simply wanted to stake his ETH and let a platform handle all the rest, from managing his assets to maximizing his rewards?

User-friendly platforms provide interfaces to simplify managing these staking investments, improving the user experience for investors like Joe.

Each service offers unique features and benefits tailored to different staking preferences, such as:

• EtherFi: focuses on self-custody and decentralized staking for individuals who want to stake their ETH securely. Its UX is tailored for users who want hands-on management of their staking without relying on intermediaries.

• Renzo Protocol: acts as a liquid restaking hub within the EigenLayer, enabling users to earn additional yields on their staked ETH. It streamlines the restaking process, across multiple blockchains (such as Arbitrum, Linea, and others) abstracting the complexity for end-users.

• Puffer Finance: provides a secure path to staking with anti-slashing mechanisms and an option to boost staking rewards by leveraging DeFi applications.

• Kelp DAO: focus on improving liquidity and DeFi integration, rewarding users with their native points and EigenLayer Points.

Risks of Restaking

While restaking can offer enhanced returns on Ethereum investments, it’s important to be aware of the risks involved in making informed decisions:

• Slashing Risks: Validators failing to fulfill their responsibilities could result in stakers losing part of their staked ETH due to penalties, a process known as slashing.

• Smart Contract Vulnerabilities and Third-Party Dependencies: Bugs or failures in the smart contracts or third-party services that manage staking can lead to significant financial losses.

• Liquidity Concerns and Token Stability: Liquid staking tokens may experience liquidity issues or lose their peg to ETH during market downturns, impacting their value and the predictability of returns.

• Leveraged Restaking Risks: Leveraged restaking offered by platforms such as Gearbox or Pendle involves using staked assets to borrow funds for further staking, amplifying both potential returns and risks. A decrease in the value of the underlying assets can trigger margin calls or liquidations, particularly during volatile market conditions, leading to substantial losses.

Closing Thoughts: The New Era of Ethereum Restaking

As the Ethereum (re)staking landscape evolves, LRT platforms like Ether.Fi, Renzo Protocol, Puffer Finance, and Kelp DAO are not only enhancing the staking process but also incentivizing participation by offering their own reward tokens or points. These rewards, which may become tradable tokens in the future, echo the early days of initial coin offerings (ICOs), providing speculative value alongside the practical benefits of staking. This dual promise of security and potential profit drives the increasing interest in decentralized finance solutions.

This article has offered a comprehensive guide to enhancing your Ethereum investment strategy, from exploring diverse staking mechanisms to navigating innovative liquid staking platforms. As the blockchain landscape continues to evolve, these platforms provide valuable tools for maximizing returns and securing assets, ensuring users can participate in and benefit from the growing potential of decentralized finance.

Acknowledgments

Thanks to Yura Sherman for bridging my consciousness with the Restaking realm and for a thorough review of the article and his valuable remarks, corrections, and insights.

If you’re new to EigenLayer and want to understand the basics of staking and restaking on this platform, read EigenLayer: A Beginner’s Guide to Enhancing Ethereum Rewards Through Staking and Restaking.

Find me on LinkedIn, Telegram, X (a.k.a. Twitter), Farcast.