Join Nostr
2026-09-24 20:57:28 UTC

Devine Lu Linvegan on Nostr: Something kind of funny happened today. In the Uxn mailing list, someone wrote a Lean ...

Something kind of funny happened today.

In the Uxn mailing list, someone wrote a Lean implementation, and through the formal verification found a little behavior difference between two emulators, and shared a 5 lines patch of Uxntal code, which I saw with my own eyes, an extremely simple patch, so simple it would be hard to deviate from this tiny bit of code to fix the issue. Especially since I have SEEN it.

While the author's repository didn't have Claude signed commits, there were signs that it might have been reached with the help of LLMs. Since this is a core utility, I didn't want to merge it straight, but letting this open is also kind of silly(the sort of stuff that keeps me up at night), although in the future, it's what I'd do: wait until someone stumbles across the bug naturally if I can.

Anyhow, with 's help, we did a little experiment. At that moment, Erik had not yet seen the possibly tainted issue nor patch, so maybe there's a way out of this. I knew where the issue was, but I am tainted at this point, so I can't fix it myself. So, I explained very broadly what the issue was, and Erik whom I trust to be a person, wrote a patch for it.

It's a strange position here, because I moderate the mailing list, so I need to read the posts, but my reading of the posts also reveal to me, possibly, issues that might not be found without LLMs, but seeing it makes me a aware of issues that suddenly I don't want to fix because I didn't genuinely found the issue. Ha! I don't even know what point I'm trying to make with this.. SOFTWARE IS HARD

https://lists.sr.ht/~rabbits/public-inbox/%3C20260924180459.2282620-1-d6@phial.org%3E#%3C45800197-a38e-47ee-b65a-01df3379ae59@100r.co%3E