0 blocking | 1 actionable, 1504 structural
Project Actionable Structural Notes z4 1 512 gamma-crown 0 345 lean5 0 371 upstream fork tla2 0 276 upstream fork
Andrew Yates · Director, AI Labs · Dropbox
ayates@dropbox.com
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.