AST hashing & effects are both used in Unison, if you want to check that out. I don't know that they have any proof-land stuff, though.