The comments mostly bought that premise. Several people with theorem-prover experience said the jump is real. Work that used to take days or weeks can now collapse into minutes on the right problems. People also pointed out that this is less revolutionary inside formal methods than it looks from the outside. Proof assistants already relied on heavy automation through tactics, SMT-backed tools, and systems like
Sledgehammer. LLMs look powerful because they can drive that machinery at a much higher level and write the connective tissue humans used to spend most of their time on.
Where the discussion landed was on limits. The hard part is shifting, not disappearing. A verified program can still faithfully implement the wrong thing if the specification is wrong, incomplete, or tied too closely to the current implementation. Multiple comments gave the same warning from different angles. Tests can all pass for a backwards feature. A formal proof can be perfectly valid for a broken spec. For most production software, the real missing artifact is not the proof. It is a precise statement of what should happen under ugly edge cases like malformed input, transient network failures, rollback, or data restoration.
That is why the most convincing near-term use cases were narrow properties rather than full correctness. Instead of proving a whole billing system is semantically right, commenters wanted assertions like “this code never executes attacker-controlled instructions,” “this path never sends secrets over the network,” or “serialize then deserialize is a round trip.” Those are understandable, portable between projects, and strong enough to eliminate expensive bug classes. Critical industries that already write formal requirements for certification were repeatedly cited as the natural place this gets deployed first.
There was also a practical split over how to structure verified software. Some argued that dependently typed code becomes a maintenance trap when every new invariant gets threaded through existing types and proofs. Others pushed back that this is exactly what correctness feels like when you stop hand-waving, and that the right pattern is to keep the trusted, verified core small while letting broad classes of ordinary code inherit its guarantees. Examples like
seL4, Rust’s borrow checker, verified crypto assembly,
CakeML,
Dafny,
Verus, and
LiquidHaskell kept surfacing as evidence that the field already has useful building blocks. The emerging view was sharp: LLMs did not make formal methods universal overnight, but they may have made them cheap enough to become normal for critical kernels, parsers, compilers, crypto, protocol code, and security boundaries first.
imperialviolet.org