Hey Gophers! I just released the first beta of go-z3, a Go binding for the Z3 SMT solver.
If you’ve ever tried to do formal verification or complex constraint solving in Go, you might have noticed that piping to a sub-process is a huge bottleneck. I’ve implemented this using direct CGO bindings to make it fast enough for real-time analysis tools.
It handles the tricky CGO memory management for you, so you can just focus on the logic. Check it out if you’re into formal methods or automated reasoning!