Software Verification and Analysis Using Z3

• souper

  12 2,071 3.4 C++

  A superoptimizer for LLVM IR

  

Google's one step ahead of you there :)

https://github.com/google/souper

• z3_tutorial

  1 147 0.0 Jupyter Notebook

  Jupyter notebooks for tutorial on the Z3 SMT solver

I'm giving a tutorial in a couple of days. Vids will be up later.

https://github.com/philzook58/z3_tutorial

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

• lean4

  52 3,714 9.9 Lean

  Lean 4 programming language and theorem prover

  

The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4

Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/

Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib.

This is an awesome mix of raw speed, functional programming, and formal software verification.

• ivy

  1 200 6.5 C++

  Discontinued IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness. (by microsoft)

  

- Ivy: https://github.com/microsoft/ivy

Suggest a related project