Kev (Oct 04 2026 at 18:28): Kev (Oct 04 2026 at 18:28):Hi,
I was playing around with formally verifying some parts of cranelift using AI, with minimal steering(every other day or so). So far two discrepancies have popped up when the AI was trying to create proofs.
One of them is this: https://github.com/bytecodealliance/wasmtime/pull/14525 and the other is https://github.com/bytecodealliance/wasmtime/pull/14526
Would be great to get some feedback on them. @bjorn3 has looked at the 14525, so potentially just focussing on that one since it has a higher chance of not being a false positive.
Thanks
bjorn3 (Oct 04 2026 at 18:30):(might have been better suited for #cranelift. looks like unlike the rust-lang instance, this zulip instance doesn't allow me to move messages between channels though, only moderators and up are allowed to)
Kev (Oct 04 2026 at 18:31):ah apologies, not sure I can move it either
bjorn3 (Oct 04 2026 at 18:34):No worries. I'm sure a mod will move it once it is no longer weekend.
Notification Bot (Oct 04 2026 at 22:48):This topic was moved here from #general > atomics cas bug by Alex Crichton.
Last updated: Oct 11 2026 at 02:20 UTC