story

Show HN: Formal – Formal verification for AI-generated code using Lean 4 (opens in new tab)

github.com

4 pointsyamafaktory1mo ago4 comments

4 comments

sjdv198229d ago

I was initially very excited about this, but looking at the code: https://github.com/yamafaktory/formal/blob/4f95787ceeabb0f09...

To extract properties to verify... you call Claude??

yamafaktoryOP29d ago

Well, I can understand your frustration, but this is basically a pipeline that takes some code written by an LLM and attempts to prove its correctness using the Lean 4 theorem prover.

sjdv198229d ago

How does your reply relate to my comment?

1 more reply

j / k navigate · click thread line to collapse

4 comments

sjdv198229d ago

I was initially very excited about this, but looking at the code: https://github.com/yamafaktory/formal/blob/4f95787ceeabb0f09...

To extract properties to verify... you call Claude??

yamafaktoryOP29d ago

Well, I can understand your frustration, but this is basically a pipeline that takes some code written by an LLM and attempts to prove its correctness using the Lean 4 theorem prover.

sjdv198229d ago

How does your reply relate to my comment?

1 more reply

j / k navigate · click thread line to collapse