pschanely/CrossHair
View on GitHub ↗ ★ 1,341 Python
An analysis tool for Python that blurs the line between testing and type systems.
11 mentions on Hacker News by 9 people: 3 stories, 8 comments · first 2020-01-15 · latest 2026-03-17
20082026
-
…An analysis tool for Python that blurs the line between testing and type systems https://github.com/pschanely/CrossHair : > If you have a function with type annotations and add a contract in a supported syntax, CrossHair will attempt to fi
comment by westurner · 2026-03-17 · in Comparing Python Type Checkers: Typing Spec Conformance -
This is exactly what the CrossHair library does: https://github.com/pschanely/CrossHair It also overloads other methods to provide kind of symbolic objects.
comment by tracnar · 2024-12-24 · in Symbolic Execution by Overloading __bool__ -
…tool for checking Python contracts using an SMT solver (using symbolic inputs over concrete paths): https://github.com/pschanely/CrossHair That said, these days I think property-based testing gets you the ~same benefits as contracts, and…
comment by pschanely · 2024-11-14 · in Contracts for C++ (DbC) [pdf] -
…looks like CrossHair[0] is a similar tool that uses Z3 to find counter examples for predicates. [0] https://github.com/pschanely/CrossHair
comment by usagitoneko97 · 2021-06-01 · in Pynguin – Generate Python unit tests automatically -
…the type annotations can be directly used. (I'm one of the authors of icontract-hypothesis.) [1] https://github.com/pschanely/CrossHair [2] https://github.com/mristin/icontract-hypothesis
comment by mristin · 2021-06-01 · in Pynguin – Generate Python unit tests automatically -
There's a tool for verification of Python programs based on contracts which uses Z3: https://github.com/pschanely/CrossHair You can use it as part of your CI or during the development (there's even a neat "watch" mode, akin to…
comment by hypernovawebant · 2021-05-04 · in Programming in Z3 by learning to think like a compiler -
…of your SMT-based projects, I'd love to compare your SMT solver notes with my mine from working on https://github.com/pschanely/CrossHair Sadly, there aren't a lot of resources on how to use SMT solvers well .
comment by pschanely · 2020-12-24 · in Finding Software Bugs Using Symbolic Execution -
…or if there are other ways to achieve that. But a similar tool for Python does it exactly this way: https://github.com/pschanely/CrossHair "CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a…
comment by anentropic · 2020-06-13 · in Static Analysis