# \[ANN\] Satisfiability.jl: a simple interface to theorem provers using the SMT-LIB standard

**URL:** https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984
**Category:** Package Announcements
**Tags:** package, announcement
**Created:** [August 19, 2023, 4:38pm UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984 "2023-08-19T16:38:42Z")
**Posts on this page:** 1
**Showing post:** 3

<div class="post-metadata">

### Author: ![Sukera](https://avatars.discourse-cdn.com/v4/letter/s/ce7236/32.png) [@Sukera](https://discourse.julialang.org/u/Sukera)
#### Post date: [August 27, 2023, 8:10am UTC](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984/3 "2023-08-27T08:10:31Z")

</div>

> [@elsoroka](#):
>
> [GitHub - elsoroka/Satisfiability.jl: Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.](https://github.com/elsoroka/Satisfiability.jl/)

Fantastic stuff! For all those folks who liked [PropCheck.jl](https://discourse.julialang.org/t/ann-propcheck-jl/101481) (which is just a fancy fuzzer), _this_ is the mathematically correct theorem proving counterpart!

Do you have plans for depending (weakly) on Z3.jl or other solvers like cvc5, so that users don’t have to install the solver through their system package manager and instead can just use a JLL from Pkg?

As for the name - I think it’s fine, since this is more or less an interface package. Kind of like Tables.jl is an interface package.

---

_[View the full topic](https://discourse.julialang.org/t/ann-satisfiability-jl-a-simple-interface-to-theorem-provers-using-the-smt-lib-standard/102984)._