Pakala: yet another EVM symbolic execution tool

Tested on Ubuntu 20.04,python 3.8.10
there were several dependencies issues on Ubuntu 22 with Python 3.10 so downgraded version is recommended for proper run
Pakala is a tool to search for exploitable bugs in Ethereum smart contracts.
Pakala is a symbolic execution engine for the Ethereum Virtual Machine.
The intended public for the tool are security researchers interested by Ethereum / the EVM.

It basically looks for ways to get money out of the contract, into an address the attacker controls. That’s the most obvious kind of vulnerability that people would seek to exploit.
What does it looks for?
Right now, there are only two built-in analyses:

call suicide() to an user-controlled address.

send() more ethers than the attacker sent.

Pakala can stack an arbitrary number of calls to the contract, to allow for state-changing calls first, and then withdrawals.

Z3 abstraction layer
It uses Z3, but through Claripy, which is an abstraction layer that exposes a nice interface, and does caching and black magic.

I also added a SHA3 layer on top of it, which does what’s needed to support cryptographic hashes properly, without this detail leaking anywhere in the code

Two layers: finding executions and stacking them

The first one executes a contract and tries to find a list of “outcomes”. An outcome is a valid execution of the contract that led to a state change (storage written, or money sent), associated to the precondition that needs to be satisfied for this specific execution to trigger.

The second layer is able to tell whether an outcome is doing something bad, corresponding to a vulnerability.

It can also stack multiple outcomes on top of each other, to simulate a sequence of multiple calls to the contract. That means it’s able to detect vulnerabilities that need more than one transaction (typically, changing the owner, then calling an “ownerOnly” function).

This approach allows it to only execute the contract once, and then focus on stacking the outcomes, which is pretty efficient. However, that means there is no support for calling external contracts. It will never be able to find reentrancy bugs either.

You can use it as a reverse engineering tool: by simply listing the outcomes it is possible to get a good understanding of what the contract is doing.


root@CryptoXploit:~# apt update
root@CryptoXploit:~# apt install python3-pip

root@CryptoXploit:~/Pakala# pip3 install –upgrade pip
root@CryptoXploit:~# pip3 install pakala

you will be required web3 API to pull latest address status, transactions etc so for that reason go to and free signup for API
setup the Ethereum API as mainnet and then go to

copy the HTTPS link

Program Run

root@CryptoXploit:~/Pakala# WEB3_PROVIDER_URI=’’
root@CryptoXploit:~# pakala 0xeBE6c7a839A660a0F04BdF6816e2eA182F5d542C –force-balance=”1 ether”

Leave a Reply

Your email address will not be published. Required fields are marked *



eclambda is a set of tools for computing elliptic curve interval discrete



This is great GPU based tool Tool for solving misspelled or damaged Bitcoin

You May Also Like