Discover is a static anlaysis and formal verification framework for computer software with many great features including:

  • Automatic execution
  • Detection of multiple bug types
  • Compatibility with multiple programming languages
  • Ease of use

Check out our featured Overview and Approach for more information


Discover is a static analysis and formal verification tool that can automatically find security bugs and vulnerabilities in programs written in both general-purpose programming languages, such as C, C++, Go, and domain-specific languages, like Solidity (for writing smart contract).

Memory Bugs

Memory Leaks, Null Pointer Dereference, Buffer Overflow, etc.

Integer Bugs

Integer Overflow, Integer Underflow, Division by Zero, etc.

Smart Contract Bugs

Reentrancy, Out of Gas, etc.


Discover is developed using the OCaml programming language. It includes two main parts.

  1. Compiler front-end: this module will compile input programs (written in C/C++, Java, Go, Solidity, etc) to intermediate code of LLVM framework (LLVM bitcode).
  2. Analyzer back-end: this module will apply suitable analysis techniques to detect each kind of bug and vulnerability. For example, we use separation logic to find memory bugs, abstract interpretation and data flow analysis to find integer bugs and other bugs specific to detect smart contracts.

Ease of use

We have provided a detailed documentation as well as specific code examples to help new users get started. Feel free to contact us if you have any query regarding the use of Discover.