angr/claripy

An abstraction layer for constraint solvers.

Python

334

2,555 commits

updated Sep 21, 2026

README

claripy

Claripy is an abstracted constraint-solving wrapper.

Project Links

Project repository: https://github.com/angr/claripy

Documentation: https://api.angr.io/projects/claripy/en/latest/

Usage

It is usable!

General usage is similar to Z3:

>>> import claripy
>>> a = claripy.BVV(3, 32)
>>> b = claripy.BVS('var_b', 32)
>>> s = claripy.Solver()
>>> s.add(b > a)
>>> print(s.eval(b, 1)[0])

Contributors

(top 30 of 68)

883 commits

466 commits

187 commits

187 commits

Similar repos

angr/angr

A powerful and user-friendly binary analysis platform!

9,102

angr/pyvex

Python bindings for Valgrind's VEX IR.

380

0vercl0k/z3-playground

A repository to store Z3-python scripts you can use as examples, reminders, whatever.

282

potassco/clingo

🦉 A grounder and solver for logic programs.

835

makaimann/smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by…

141

Boolector/boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays…

359

GaloisInc/cryptol

Cryptol: The Language of Cryptography

1,221

ampl/mp

An open-source library for mathematical programming

254

Languages

Python

100.0%

angr/claripy

An abstraction layer for constraint solvers.

Python

334

2,555 commits

updated Sep 21, 2026

README

claripy

Claripy is an abstracted constraint-solving wrapper.

Project Links

Project repository: https://github.com/angr/claripy

Documentation: https://api.angr.io/projects/claripy/en/latest/

Usage

It is usable!

General usage is similar to Z3:

>>> import claripy
>>> a = claripy.BVV(3, 32)
>>> b = claripy.BVS('var_b', 32)
>>> s = claripy.Solver()
>>> s.add(b > a)
>>> print(s.eval(b, 1)[0])

Similar repos

angr/angr

A powerful and user-friendly binary analysis platform!

9,102

angr/pyvex

Python bindings for Valgrind's VEX IR.

380

0vercl0k/z3-playground

A repository to store Z3-python scripts you can use as examples, reminders, whatever.

282

potassco/clingo

🦉 A grounder and solver for logic programs.

835

makaimann/smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by…

141

Boolector/boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays…

359

GaloisInc/cryptol

Cryptol: The Language of Cryptography

1,221

ampl/mp

An open-source library for mathematical programming

254

Contributors

(top 30 of 68)

883 commits

466 commits

187 commits

187 commits

Languages

Python

100.0%