Skip to main content

Analyze Python code for correctness using symbolic execution.

Project description


Join the chat at codecov Check status

An analysis tool for Python that blurs the line between testing and type systems.

Marko Ristin just published an early VS Code extension for CrossHair! Install it from the VS Code Marketplace.

If you have a function with type annotations and add a contract in a supported syntax, CrossHair will attempt to find counterexamples for you:

Animated GIF demonstrating the verification of a python function

CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you. This is not a new idea; an approach for Python was first described in this paper. However, to my knowledge, CrossHair is the most complete implementation of the idea: it supports symbolic lists, dictionaries, sets, and even symbolic instances of your own classes.

Try CrossHair right now, in your browser, at!

NOTE: CrossHair is in an experimental state right now. You can help though!


Available at

Project details

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Files for crosshair-tool, version 0.0.11
Filename, size File type Python version Upload date Hashes
Filename, size crosshair_tool-0.0.11-py3-none-any.whl (160.4 kB) File type Wheel Python version py3 Upload date Hashes View
Filename, size crosshair-tool-0.0.11.tar.gz (136.8 kB) File type Source Python version None Upload date Hashes View

Supported by

AWS AWS Cloud computing Datadog Datadog Monitoring DigiCert DigiCert EV certificate Facebook / Instagram Facebook / Instagram PSF Sponsor Fastly Fastly CDN Google Google Object Storage and Download Analytics Pingdom Pingdom Monitoring Salesforce Salesforce PSF Sponsor Sentry Sentry Error logging StatusPage StatusPage Status page