A symbolic execution engine for EVM and explorer for K-framework reachability proofs.
**This is an early alpha version for internal usage. Direct any questions in an issue or at https://dapphub.chat/channel/k-framework .
You will need a modified version of evm-semantics, containing a modified version of k:
- https://github.com/dapphub/evm-semantics use the
klabbranch
Install it with:
make deps
make
git clone [email protected]:dapphub/kdebug.git
cd kdebug
make
Export path variables e.g. save them in ~/.profiles
export KLAB_K_PATH=/path/to/k
export KLAB_EVMS_PATH=/path/to/evm-semantics
You also need to set the temporary directory to use, for example:
export TMPDIR=/tmp
Write a spec.ini file with the property you want to prove and put it in a directory together
with the solidity source code file together with the corresponding .sol.json.
From the same directory, run:
klab run
to start the klab interactive tool.