kompass is a CLI application that performs and manages symbolic execution and proofs of Rust programs for the Solana ecosystem using a Rust semantics written in K Framework.
python >= 3.10,pip >= 20.0.2,uv >= 0.7.2(other versions may work, too).
make build
pip install .kompass operates inside a cargo project to build and run/prove the code in it and view proof artifacts.
For basic usage information, run kompass --help and inspect each command's available options with kompass <command> --help.
See Usage.md for more detailed instructions including a small example program.
kompass depends on the K Framework Rust semantics mir-semantics
and the stable-mir-json plugin to rustc.
Using kompass requires an installation of stable-mir-json (on the path under this exact name or installed in $HOME)
and the build tool cargo (on the path under this exact name).
kompass is developed and tested on x86_64 platforms with Ubuntu Linux but should work on other 64bit POSIX systems where cargo and rustc are available.
Use make to run common tasks (see the Makefile for a complete list of available targets).
make build: Build wheelmake check: Check code style and formattingmake format: Format codemake test: Run tests
For interactive use, spawn a python interpreter with uv run -- python3 (after uv venv).