Seaverify - formal verification for Solana smart contracts
Tldr: I believe it’s a relatively low hanging fruit to massively improve the current state of art of formal verification of Solana smart contracts, by creating a tool specially made for smart contracts, that automatically verifies properties specified by programmers with z3.
My previous attempt to write that for Seahorse (python that compiles to Anchor code): GitHub - coqlover/seaverify
Chat location: I don’t have for now a discord. Please reply here or on Twitter
Formal verification is somewhat the current hype of twitter Ethereum, multiple tools exists and it seems to work fine. But almost no attempt was made to verify Solana smart contract code. I wish to fix that.
The only (to the best of my knowledge) attempt to verify Solana smart contracts is an OtterSec article named “formally-verifying-solana-programs”. This article is very nice, and effectively prove properties on a multisig program. Very nice.
I believe a similar approach can bring formal verification to the mass. There are few challenges to that.
First, make it easy for anyone to write properties that will be verified. This is ok. For instance, for Rust, there is for instance creusot where it’s easy to annotate programs. In my attempt in Python, annotations are with decorators. It’s intuitive too.
Second, the verification should work if the contract is simple. This is the tricky part, performance of solvers is insanely unpredictable. For instance, if you write yourself sha256, and ask it if “a != b => hash(a) != hash(b)” it will just timeout. No luck if you need this property somewhere in your contract (without being aware you actually need it).
I personally believe these problems are in finite number (after all the number of really different contracts is quite small), and by customizing a tool for smart contracts you make them all disappear. For hash function, it’s “”“safe”“” to assume the property above for instance.
A more concrete example of that is proving properties about AMMs, I wrote a bit about it on medium (my username is coqlover on medium). Performance depends a lot on how you “use” the tool. I believe It’s unrealistic to expect programmers to do it, it makes more sense to have a library already written for that. And no one will ever use a tool that timeouts on a simple AMM/whatever example.
Another required transformation is removing all the generated code by Anchor, and only verifying the code actually written by the user. This requirement makes it hard to directly apply existing verification tool, or at least it requires some work to do it.
I like Python, so I started to build on Seahorse, but the type system of Rust makes it more easy to build there, and everyone writes their code with Anchor, hence the switch of direction.
I believe that if the verification made by seaverify have predictable and good performance (a big assumption for sure), then thanks to its intuitive syntax, it will be quickly adopted by programmers.
If you are interested in the project, or have any suggestions, let me know!
Here are some screenshots of my current try on Python: Imgur: The magic of the Internet