In the previous post, we showed how to prove the correctness of Mint operation which is part of the basic functionality of both the SPL Token. In this post, we show how the Solana Certora Prover (SCP) can be used to find bugs in the confidentiality extension of the SPL Token.

The Certora team recently finished reviewing token extensions on Solana utilizing our in-depth formal verification tools.

In our previous post, we described our new verification tool for Solana contracts. In this post, we show the verifier in action on SPL Token 2022, a widely-used Solana application. In the next post, we will show how to find bugs in the confidential extension of SPL Token 2022.

In a series of posts, we shall discuss our efforts to formally verify Solana smart contracts. We have developed a new in-house verification tool that takes Solana contracts written in Rust together with a specification and automatically proves that the specification holds.

Certora today announced its engagement with Solana Foundation to review and formally verify the code underlying token extensions on Solana, the new program-level token features that natively extend token functionality.