Launched this week
Logician

Logician

Type-safe SMT solver driver for Rust—no C++ toolchain needed

2 followers

Visit website
Logician lets Rust developers use SMT solvers like Z3 and CVC5 without compiling C++ bindings. Build formulas with a fluent API that catches sort mismatches immediately. Z3 times out? Auto-retry on CVC5. Hung solver? Watchdog kills it. ✓ Type-safe Term API with runtime invariants ✓ Multi-solver fallback ✓ Process watchdog with clean termination ✓ Optional async (tokio) ✓ MIT licensed, free forever Perfect for constraint solving, verification, and SAT/SMT without FFI pain.
Logician gallery image
Logician gallery image
Free
Launch tags:Productivity•Open Source•Developer Tools
Launch Team
Famulor AI
Famulor AI
One agent, all channels: phone, web & WhatsApp AI
Promoted

What do you think? …

Mike Kuykendall
Maker
📌
Hey PH! 👋 I built Logician because using Z3 from Rust was either: 1. FFI bindings → C++ toolchain hell 2. String-based → pray your SMT-LIB parses Logician is a subprocess driver. You install Z3 normally, and Logician talks to it via stdin/stdout with a type-safe Rust API. What it does: • Panics immediately if you mix Bool and Int terms • Tries Z3, falls back to CVC5 if it fails • Kills hung solvers (no orphan processes) What it doesn't do: • Arrays, bitvectors, quantifiers (use FFI for those) • Be a solver itself (you bring Z3/CVC5/Yices) Would love feedback from anyone doing formal verification, constraint solving, or just curious about SMT!