Formal Security Verification for Smart Contract.



RK87 is a symbolic platform for Solidity smart contracts. User can add assertions and assumptions into existing Solidity code base to let symbolic engine search for counterexamples or get verified.

RK87 is the only platform that allow user to do symbolic verifier using only Solidity language and some small support directives.

How it works?

RK87 first compiles Solidity source code into symbolic represents, and then Z3 symbolic execution engine will be used to perform analysis. Additional directives can be added to support declarations and verifications.


Please refer to RK87 Documentation for examples and to learn more about all supported directives.

Are you looking for Smart Contract Security Audit Services?

Contact us


Smart Contracts Massive Hunting for Vulnerabilities

Our paper, Smart Contracts Massive Hunting for Vulnerabilities, at JD-HITB Security Conference Beijing 2018 shows  a new approach to finding security bugs in smart contracts using symbolic execution that is not pattern-based. Early results are promising: the tool managed to accurately detect most smart contract security bugs reported in 2018 and has helped us find many unpublished ones. Read more

Monocerus: Dynamic Analysis for Smart Contract

Nguyen Anh Quynh, Monocerus: Dynamic Analysis for Smart Contract, BlackHat Asia 2019. Read more