[Animats]

Yes. I dealt with them a lot in my aerospace days.

Boyer and Moore used to work there. I used their theorem prover for early proof of correctness work.