Andrew Yates · Director, AI Labs · Dropbox
[email protected]
All d* projects are entirely AI generated.
Proof is the only scalable code review. AI generates code faster than humans can review it. But we don't need to understand the code or remember the proof — we just need to verify that a proof exists. These tools make verification practical: SMT solvers check constraints, model checkers explore state spaces, theorem provers verify logic.
| Project | What it does | Version |
|---|---|---|
| z4 | SMT solver in Rust. SAT/SMT engine with theory solvers, CHC, QBF, MaxSAT. Parses SMT-LIB 2.6, produces DRAT/LRAT proofs. The foundation everything else builds on. | Active |
| tla2 | TLA+ model checker. Drop-in TLC replacement — single binary, no JVM. 97.5% state-count parity across 160 specs, zero false positives. | v0.1 |
| gamma-crown | Neural network verifier. Proves robustness and safety properties of neural networks. pytest for models — finds exactly where your model broke. |
v1.0 |
| lean5 | Theorem prover in Rust. Lean 4 reimplementation with sub-microsecond type checking and 1M ops/sec throughput. Designed for AI agents that need real-time proof verification. | Preview |
Apache 2.0 — See LICENSE for details.
See RELEASES.md for version history.