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.

The Mechanics Behind iUSD Redemptions in infiniFi

When users deposit USDC into infiniFi, they receive iUSD tokens. Users can then choose to:

• Convert iUSD into siUSD for immediate liquidity (redeemable at any time).
• Convert iUSD into liUSD-xw, locking it for governance power and enhanced yield multipliers.

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.

Bypassing the redemption queue 

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: 

• Block N: Alice calls to redeem for 100. Since there is no liquidity available, a redemption request is added to the redemption queue.
• Block N+1: Liquidity in the system increases by 100 due to collected yields. 
• Block N+1: Bob calls to redeem for 100. Since there is 100 liquidity available, he instantly receives his funds. Alice’s redemption request remains in the queue.

This violates FIFO ordering and exposes Alice unfairly to slashing.

Formally Verifying Fairness with the Certora Prover 

To capture and enforce the FIFO behavior, our security researchers and formal verification engineers wrote a precise rule using the Certora Prover:

Rule: no_immediate_redemption_from_non_empty_queue

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.

Fixing the queue for fairness

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.

Key section from the fixed version:

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.

Verification Outcome

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:

• No instant redemption can occur when the queue is non-empty.
• Users in the queue are prioritized before new requests.
• FIFO ordering is consistently enforced.

This provides formal assurance that the bug has been fully mitigated and the redemption behavior now aligns with the protocol’s fairness goals.

Why does this matter?

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.

• Redemption queues must be prioritized to ensure the fair FIFO ordering is respected and users are not unfairly subjected to slashing.
• Formal specifications help encode fairness properties, making them enforceable rather than aspirational.
• Certora Prover enables pre-deployment detection of business logic violations, making it especially valuable in protocols with complex state transitions or liquidity constraints.
• Post-fix re-verification is essential to confirm that the intended behavior is restored.

Conclusion

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