This makes sense, although it's not well described here.

Formal methods, as in proof of correctness, have been around for decades (I was doing that stuff in the 1980s) but pushing the proofs through was too laborious. The seL4 verification effort reportedly used over a decade of people time.

The idea is that if you have a formal specification of what you want to happen, you can get a LLM to do the struggling with the proof system to get it right. It's a good task for an LLM, because there's feedback from the prover.

I'd like to see more non-trivial examples of this. People keep republishing verifications of greatest common divisor or stack algorithms, which was done decades ago.

▲

gritzko 7 hours ago | parent | next [-]

might be relevant: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...

	▲	Animats 7 hours ago \| parent [-]
		Yes. I should have cited that. He has this right.

▲

oulipo2 7 hours ago | parent | prev | next [-]

Problem is, usually describing the problem you want to solve *correctly* using formal tool is a task as hard (and often, equivalent to) the implementation. That said, having a formal description is useful

▲

Animats 7 hours ago | parent [-]

For some problems, yes. Formal specification is particularly useful in two cases. 1) The problem is simple but an efficient implementation is hard or bug-prone. Examples are garbage collection, file systems, sorts, databases, and tree updating. 2) The inverse of the problem is simpler than the forward operation. Examples include matrix inversion and parsing.

▲

auggierose 7 hours ago | parent [-]

I wouldn’t split it like that. Formal verification is useful in the case that the spec is simpler than the implementation. That’s it.

Coming up with simple specs is not necessarily easy. You could say that is kind of what math is about. That’s how we actually make progress: find those cases where simple specs are possible and build upon them. That’s the kind of library made for eternity.

▲

oulipo2 4 hours ago | parent [-]

It could still be useful if the spec is roughly as hard as a simple implementation, in case you have automated methods to find more efficient implementations, guided by the constraints of the spec

	▲	auggierose 3 hours ago \| parent [-]
		Which is still a case of the spec being simpler than the implementation (you are after) ;-) Very often, the spec is indeed just a very simple implementation. Often you can make the spec especially simple if there are no constraints on the resources it can use, at times even infinite ones.

▲

7 hours ago | parent | prev [-]

[deleted]