> I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction,

Exactly right!

More details in my comment here - https://news.ycombinator.com/item?id=49269323

See also, Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - https://mitpress.mit.edu/9780262528900/software-abstractions...