z3overlay

Tech stack & purpose

z3overlay is an overlay for the OCaml Z3 binding that enhances the official Z3 binding with type-level tracking of SMT solver terms. Built in OCaml using generalized algebraic data types (GADTs), it allows the OCaml type system to verify the validity of Z3 formulas at compile time and simplifies model extraction. Z3 itself is an SMT solver developed by Microsoft, and this package wraps it to provide safer, more ergonomic access from OCaml code.

Community & reference links

• Z3
• termite-analyser.github.io/z3overlay/

Languages

Contributors

• 
  Gabriel Radanne64 commits · 222 followers
• Bruno FERRES2 commits
• 
  Gabriel Radanne1 commits · 222 followers