Title: [TEMP CHECK] Port of Aave to Solana using Formal Verification
Author: @guillaumeclaret
Date: 2025-12-04
Summary
This is a post to discuss the idea of porting the Aave protocol to Solana using formal verification to ensure the business logic is the same in both implementations.
Motivation
Porting Aave to more platforms enables attaining more users, but it also creates additional maintenance costs and security risks, especially when the programming paradigm is so different as in Solana.
Formal verification is a technology that we think helps reduce the risk in building a Solana port, as it is possible to check the equivalence of two contracts, EVM and Solana-based, for all possible inputs, up to an abstraction of the changes needed for the two ecosystems (ERC-20 vs Solana Token, for example). An important part of a contract that does not change between platforms is the purely computational part, with the mathematical rules to compute the amounts, which can be verified as being exactly the same, independently of the platform.
Proposed Solution
At Formal Land, we developed tools to formally verify both Solidity and Rust code in a common backend, the Rocq theorem prover, and think this project is within reach of current technology. A Solana port being proven equivalent to the EVM version would inherit a lot of its security properties and time-proven robustness.
What do you think about this idea?
Next step
Implement the idea on a small part of the code, for example a math component.
Copyright
Copyright and related rights waived via CC0