Ghost of Departed proofs provides a fairly trivial way to generate proofs from arbitrary code and track them in the type system. See this article for example: https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized...

This post shows a simple "positive" assertions, without any combinatorial logic associated with the proofs. But this is similar to programming by contracts.