Very Interesting!

Do you have a detailed paper/article written on this?

> I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.

This is not completely clear; would you mind elaborating on that in more detail?