Liquid Collective Completes Full Formal Verification

Liquid Collective has completed a formal verification audit of its ETH liquid staking protocol, including all smart contracts; this was conducted by Certora, an industry-leading provider of formal verification tools and smart contract audits, and included a conventional smart contract audit of new protocol deployments. The final changes to remediate the audit’s findings were included in the recent v1.2.1 Liquid Collective protocol upgrade, which also included other improvements.

The formal verification audit of the Liquid Collective protocol included:

• Ensuring the correct accounting of staked ETH and the Protocol Conversion Rate
• Validating the correctness and integrity of the LsETH redemption process
• Verifying the reliability and data integrity of Oracle reports
• Confirming proper management of validator keys and operator states.

Full formal verification follows the Liquid Collective Quantstamp audit and provides additional peace of mind for Liquid Collective’s users, representing the ninth security review of all code deployed to mainnet. It demonstrates that the protocol is likely to function correctly under all conditions and has a reduced risk of unexpected bugs and vulnerabilities.

How Does Formal Verification Work?

A formal verification audit assesses the correctness of algorithms within a system, determining code robustness and assessing security.

Unlike traditional code testing methods, completing full formal verification provides mathematical assurance that the system—in this case, Liquid Collective’s ETH liquid staking protocol—behaves as expected under all possible conditions.

In traditional audit and testing methods, developers create a set of test cases designed to cover a range of scenarios, including typical use cases, edge cases, and known problematic situations (such as attacks that other protocols have suffered).

However, no matter how extensive, traditional testing cannot cover every possible input the protocol might encounter.

Formal verification explores every possible state and system input, validating correctness in a way that traditional testing cannot.

Formal verification is a rigorous process that can be simplified into two main steps:

1. Mathematical Modeling: Create a precise mathematical representation of the protocol and its intended behaviors.
2. Automated Analysis: Use specialized software tools to systematically examine the model and confirm that the protocol meets its specifications in all scenarios.

This approach provides a structured and comprehensive method to ensure the correctness and reliability of protocols, particularly in critical systems where errors could have significant consequences.

Additional Enhancements Included in This Upgrade

As well as full formal verification, the latest v1.2.1 protocol update deployed multiple improvements, including:

• a fix to mitigate to the low-severity node operator front-running vulnerability
• a new public read method that exposes the LsETH Protocol Conversion Rate, further unlocking LsETH DeFi integrations

LsETH in DeFi & the Protocol Conversion Rate

Unlike other liquid staking tokens that follow the aToken model (e.g., stETH), LsETH does not mint new tokens for rewards. Instead, its Protocol Conversion Rate increases to reflect ETH network rewards as they’re received.

This is because LsETH is based on the cToken model, which uses a dynamic conversion rate to represent staked ETH plus accrued rewards.

This has several positive implications, including:

• Simplified rewards: All rewards are consolidated through the Protocol Conversion Rate, instead of minting new tokens to your wallet.
• DeFi composability: cTokens are more widely adopted in DeFi.
• Auto-staked rewards: Rewards are automatically staked.

The new public read method for the LsETH Protocol Conversion Rate deployed in this upgrade will further unlock DeFi integrations for LsETH, allowing protocols like Balancer to account for the ETH network rewards that LsETH accrues while the token is being used in other DeFi applications.

Liquid Collective Will Always be Committed to Security

Completing formal verification is a milestone in Liquid Collective’s ongoing efforts to maintain the highest security and reliability standards.

Liquid Collective is, and always will be, committed to upholding enterprise-grade security standards. This gives LsETH users confidence that their interests will always be paramount as we continue to innovate and expand.

You can view Liquid Collective’s security information anytime in the protocol’s Diligence Hub.

Keep in Touch With Liquid Collective.

Liquid Collective continues to innovate in new and exciting ways. Stay up-to-date by following Liquid Collective on X and subscribing to our newsletter.