Yices

SMT engine. So help me, I'm just a sucker for this type of thing. Microsoft uses it to validate drivers (example). Anyway, Yices is an example. Background. And the trigger - a Haskell DSL for expression of SMT problems. This is the kind of thing I want to be doing here.