Testing a symbolic analyser for the TON blockchain

Bought a new token for a lot of money and then couldn't sell it; sent money to a friend's wallet, and it vanished mid-transfer—typical cryptocurrency user stories. They don't realize that under the hood of a scam are smart contracts cleverly disguised as legitimate wallets. Who tests their reliability, who checks for vulnerabilities and the possibility of losing money?

Modern testing trends favour automation. Most will mention LLMs, some will recall fuzzing. Formal methods are popular in academia, and we are no exception; our choice is symbolic execution. But how to test such an analyser?

Simple unit tests won't suffice. We write artificial contracts to check for vulnerabilities and run on real ones to check for functionality. But let's be honest: inventing this is hard, real contracts require optimization, and debugging it all is pure hell. 

Within the talk, we'll share the ups and downs of creating and testing a symbolic analyser for the TON blockchain.