Introduction

CrossHair is an analysis tool for Python that blurs the line between testing and type systems.

If you have a function with type annotations and add a contract in a supported kind of contracts, 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 custom mutable objects.

Try CrossHair right now, in your browser, at crosshair-web.org!