In this post on his personal blog, Daniel Fedorin describes his experience applying the Alloy model checker to the Chapel compiler.