Related Work

dependent types, refinement types

CrossHair aims to provide many of the same capabilities as these advanced type systems. CrossHair is easier to learn (because it is just python), but is incomplete. It can’t always tell you whether a condition holds.

design by contract

Unlike most tools for contracts, CrossHair attempts to verify pre-conditions and post-conditions before you run them.

fuzz testing, QuickCheck, property testing, Hypothesis

CrossHair has many of the same goals as these tools. However, CrossHair uses an SMT solver to find inputs rather than the (typically) randomized approaches that these tools use.

concolic testing

CrossHair is essentially a concolic testing system. This kind of tool sits in a middle ground in between property testing and formal methods.

formal methods, Nagini

CrossHair is good at finding counterexamples, but cannot generally prove that properties hold. Formal method tools can help you do that. For example, Nagini, is a verifier for Python programs.

The main downside of full verification is that you’ll need to understand a bit about how the verifier works and may need to guide it with additional information like loop invariants and termination proofs.

SMT solvers

SMT solvers power many of the tools in this table. CrossHair uses Z3.

angr, klee

Symbolic execution of binary code. Unlike these tools, CrossHair models the semantics of Python directly.

PyExZ3, pySim, PEF

These approaches that are very similar to CrossHair, in various states of completeness. CrossHair is generally more prescriptive or product-like than these tools.