Ensuring Fair Redemptions in infiniFi with Formal Verification
infiniFi is a DeFi platform that optimizes yield by managing deposits across popular protocols like Pendle, AAVE, and Ethena. Users deposit USDC and receive iUSD, a receipt token that can be staked or locked in exchange for yield. Locking durations are linked to specific epochs, with longer commitments rewarded by higher multipliers. The protocol’s modular farm setup allows it to integrate easily with various DeFi strategies, ensuring optimal returns and transparency.
Unlike traditional banking, infiniFi lets users choose exactly how much liquidity they're comfortable locking up and for how long.
When redeeming, if there is not sufficient liquidity to complete the request, the request is submitted to a first-in, first-out (FIFO) queue and processed in order as liquidity becomes available. This ensures fairness, particularly since users waiting in line may incur penalties (by slashing).
However, a formal verification check using Certora Prover, our tool designed to detect issues in smart contracts, identified an important malfunction: a new redeem request would be fulfilled while an existing redemption request would remain open. This issue, classified as a high-severity bug, has since been resolved.
When users deposit USDC into infiniFi, they receive iUSD tokens. Users can then choose to:
Internally, deposits are allocated between liquid and illiquid yield sources. When users redeem their iUSD, the system first tries to fulfill requests from liquid sources. If not enough liquidity is available, requests are entered into a queue which later gets funded. Users in the queue are eligible for slashing until their redemption is complete, making fairness crucial.
Whenever users want to redeem their funds, they call redeem, triggering the beforeRedeem hook to withdraw liquidity from the liquid yield sources to fulfill the request. A redemption request is added to the redemption queue if insufficient liquidity is present.
Queue funding is performed via admin-triggered actions, which provide the necessary liquidity for users to complete redemptions.
However, the liquidity available in the infiniFi system is highly dynamic and can increase or decrease in mere moments. Newly available liquidity was not considered for existing redemption requests, but could be utilized to fulfill new redemption requests without first considering the queue.
Example Scenario:
This violates FIFO ordering and exposes Alice unfairly to slashing.
To capture and enforce the FIFO behavior, our security researchers and formal verification engineers wrote a precise rule using the Certora Prover:
This rule asserts that if the redemption queue is non-empty, a new redemption should not result in the user receiving the full asset amount. It ensures that the system respects the priority of pending requests.
When executed on the original code, the rule failed, indicating that the system permitted queue bypassing in some cases. Testing against the original code revealed a failure, exposing instances where the system incorrectly allowed new requests to bypass the existing redemption queue.
The solution involved adjusting the redemption logic in RedeemController so that new redemption requests are automatically entered into the queue whenever the queue is not empty, regardless of liquidity availability, thus ensuring the FIFO ordering.
This simplifies the process by eliminating any need for liquidity comparison. All users are treated fairly, simplifying the process and ensuring consistent treatment for both early and late redeemers.
It's worth noting that with this change, comparing new redemption amounts to existing liquidity is no longer needed. Those who redeem early and those who redeem later receive equitable handling. Avoiding partial funding makes the process for tracking transactions more straightforward. The updated logic described here is live and active within the infiniFi platform.
After applying the fix, the same rule no_immediate_redemption_from_non_empty_queue was retested with Certora Prover. This time, it passed successfully, confirming that:
This provides formal assurance that the bug has been fully mitigated and the redemption behavior now aligns with the protocol’s fairness goals.
Fairness isn't only about security; it’s about trust and predictability in financial systems. As demonstrated here, formal verification helps detect and resolve critical issues proactively.
Formal verification ensures the integrity of key economic and governance principles, maintaining user trust in DeFi protocols.
Our engineers identified and corrected a subtle but significant issue in infiniFi's redemption logic through rigorous formal verification, ensuring fairness and trustworthiness. This highlights formal methods’ essential role in securing smart contracts and preserving fundamental economic fairness within DeFi ecosystems.
The team ensured that users are treated consistently and predictably under all conditions by encoding the intended FIFO behavior into a precise rule and verifying it against the protocol’s implementation.
Detailed findings and vulnerabilities are available in the full report: https://www.certora.com/reports/infinifi-protocol-formal-verification-report
Pamina Georgiou
Andrew Ferraioulo