Symbolic analyzer for TON smart contracts

TSA (TON Symbolic Analyzer) is a static analysis tool based on symbolic execution and designed for smart contracts on the TON blockchain.

To start using TSA, follow the guide.

To know more about the core design, read the corresponding documents.

TSA works on TVM bitcode level, so it is possible to analyze smart contracts written in any language, just need to compile it to BoC format.

TSA is designed for a few purposes:

Detect possible TVM runtime errors: Find possible misbehavior while processing integers (overflow/underflow, division by zero) and slices/builders (reading or writing wrong number of bits, incorrect types, etc).
Generate regression tests: TSA is able to generate Blueprint-based tests based on discovered execution paths that allow to fix expected behavior and find errorneous executions.
Honeypots detection: TSA can detect and report malicious contracts that are created to fool users.

TSA has been funded by the TON Foundation grant grant and has been developed under the 8-month roadmap.

TSA is inspired and is actively using the Universal Symbolic Virtual Machine(USVM) – a symbolic core engine for multiple programming languages.

USVM and TSA itself also widely use the KSMT library – a Kotlin/Java API for SMT solvers, with some optimizations for TON blockchain.

You are very welcome to contribute to both of these projects.