Let me see whether i can explain things better.

> Formal verification only guarantees consistency between the 'specification' and the 'implementation.' It does not guarantee that the 'specification' correctly reflects reality. This is a problem of modeling.

> For your logic to hold, it would imply that humans can formalize, to some degree, the amount of loss that occurs when modeling reality. That is not possible.

Not quite true.

You model reality by mapping your chosen abstractions from the problem domain onto some solution domain. The language of Mathematics was standardized so that we can communicate our problem domain concepts using a "Formal System" (i.e. set of symbols, syntax, rules etc.) to build a "Mathematical Model" (i.e. the interpretation of the above symbols in some real-world domain). The advantage here is that, the mathematical model is precise/well-defined and thus amenable to mechanical manipulation/checking using the rules of symbolic logic by a human/machine.

So the requirements engineering process identifies real-world problem domain concepts/objects/features/usecasees, expresses them using a formal system notation (eg. The Z notation language) to build a unambiguous self-consistent mathematical model. This is the "Formal Specification" for a system. Because it is unambiguous, there can be no confusion in interpretation between all stakeholders. When requirements change (doesn't matter how often), the model is updated but because it is a formal system any inconsistencies can be immediately detected and fixed to bring the system back to a self-consistent state.

The above is basically a realization of the "Scientific Method" viz. Observe, Measure, Hypothesize, Test, iterate (over all of the previous) so that you converge with arbitrary precision towards a desired mapping of your chosen reality.

In this regard see the classic essay The Unreasonable Effectiveness of Mathematics in the Natural Sciences - https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness...

> The point that 'the cost has been lowered due to AI' is largely no different from simply saying 'the cost of implementation has gone down.'

There is a subtle but important distinction. AI-generated code is probabilistic i.e. for the same exact specification/prompt every run will produce slightly different code. So verification becomes far more important in assuring system robustness i.e. correctness w.r.t. specification. Using AI-agents you can do implementation(i.e. coding) + verification as easily as implementation only. But of course you have to study formal methods and know what to do so that you can instruct an AI-agent do it.

> The OP's post is fundamentally about 'internal invariants.'

No, the OP is merely pointing to a basic conceptual idea which helps one to do formal verification i.e. invariants -> verification conditions -> proof -> theorem.

> But if you look at the beginning of the first post: 'But outside of some special cases (notably, hardware synthesis), our sense has been that formal methods were just not worth the costs for us. And those costs are really high! seL4 is a great example of this. It's a formally verified microkernel, and a profound achievement. But, boy was it expensive to do! It took 25 person-years of effort to verify 8,700 lines of C, and each line of code required something like 23 lines of proof and a half a person-day to verify.' And the post suggests extending existing methodologies. I think a limited case and generalizing it are different problems. The point is that not every special case is general. ... That is why I pointed out whether this extension of methodology is even possible. I am skeptical on this point.

This refers to difficulties using formal methods pre-AI era, because you had to learn special mathematics, methodologies and tools to use this maths all of which are non-trivial. So people only used it for critical problem domains where the labour was worth the cost. But with AI, this constraint is no longer true and so all problem domains are amenable to formal checking provided of course you get the formal specification right.

> I am asking whether modeling in the age of AI agents is comparable to modeling in the past.

Modeling in the age of AI can be done far more faster i.e. far quicker turnarounds to converge your understanding of requirements and verify it simultaneously.

> The question is whether the idealism you advocate actually reflects reality. I am simply arguing for modeling. The gap in my argument is that 'then, because modeling also changes frequently, couldn't all methodologies become useless?' That could be a potential flawed skepticism. But what you're saying is not that.

> Every argument has a blind spot. But you are not reading the weak points of my argument; you are only reading your own strong points. This only creates friction and leads us to argue about our emotional differences. I think you are intelligent and knowledgeable. But the points you're raising are not the points of criticism I intended, and what you're pointing out is not what I said.

I have already addressed these in the beginning of this post.

PS: I am assuming you wrote your above comment after your sibling comment here - https://news.ycombinator.com/item?id=48548589 I have already mentioned a couple of reference books and more can be suggested if needed. In particular, i highly recommend the "Understanding Formal Methods" book which is a fire-hose of information. It tries to provide an overview of the whole domain with chapters alternating between mathematical theory and methodologies/tools using the theory. Supplement it with wikipedia/google as needed. After this you can pick up a book/documentation on any specific tool you like eg. Dafny, Lean4, TLA+ etc. with the assurance that you understand the basic concepts and can use the tool effectively.