Programming in Z3 by learning to think like a compiler

• alive2

  4 675 9.3 C++

  Automatic verification of LLVM optimizations

  

Alive/Alive2 [1] is one of the most famous frameworks for compiler transformation verification using BitVec logic

[1] https://github.com/AliveToolkit/alive2

• recreational-rosette

  1 108 0.0 Racket

  Some fun examples of solving problems with symbolic execution

I don't know about "practical," but you might enjoy this: https://github.com/kach/recreational-rosette

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• zz

  10 1,604 1.9 Rust

  Discontinued 🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C

  

This post reminds me that I've been wanting to try out ZetZ[0]. It incorporates Z3 into a high-level programming language, and seems to do a lot of what the post talks about automatically.

[0] https://github.com/zetzit/zz

• taxoptimizer

  1 - -

I used it to do some tax optimization around ISOs at a newly public company (https://gitlab.com/mbryant/taxoptimizer/-/blob/master/amt.py). It gets pretty slow when you try to look more than a few years out, so I'm guessing writing some optimization logic by hand would've made more sense. Using Z3 here definitely beat me trying to do this on paper like I've seen other people do!

• angr

  13 7,203 9.7 Python

  A powerful and user-friendly binary analysis platform!

  

angr uses z3.

https://github.com/angr/angr

Supposedly, the DoD has used angr for some use cases.

• CrossHair

  8 944 9.2 Python

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

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 auto-correct).

Suggest a related project