Thanks for the pointer to Jai! I will check it out.

Yes, Jacquard uses content-addressed definitions and it should be possible to set up a process for 'review again if this changes' on top of it. Warp, the testing framework, already uses this to avoid rerunning pure tests when neither the definition or dependencies have changed.

Jacquard does not currently implement proof or strictness levels, but binding those to a definition’s content identity is interesting and definitely worth exploring.

What are you building that people keep comparing to Ada?

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.