[Ufmrg] Re: Bugs in theorem prover(s)

[Felix Linker <[e-mail]>]

Hi Nadim,

The change to isSafetyFormula is just defensive programming. It's not
relevant to the fix.

You can call the bug a soundness issue, if you like. I haven't made up my
mind and don't plan to.

Cheers,
Felix


Am Mi., 12. Aug. 2026 um 15:52 Uhr schrieb Nadim Kobeissi
<[e-mail]>:

> Hi Felix,
>
>  It’s debatable whether this is a soundness bug as no proof rule was
> changed.
>
>
> No, I’m sorry, let’s all be honest. Your changes to the language interface
> were insufficient, and you had to make additional fixes to
> `isSafetyFormula`, which is a soundness-related function that you added in
> 2012 specifically to check for soundness issues and to fix a soundness bug:
>
> Full details here:
>
>
> https://github.com/tamarin-prover/tamarin-prover/issues/917#issuecomment-5267310122
>
> I wish you and the Tamarin team the very best, but it’s important to me
> that the truth be recognized: this is undeniably and objectively a
> soundness issue in the Tamarin prover.
>
> I have no issues with your other comments.
>
> Thank you,
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
>
> On 12 Aug 2026, at 3:47 PM, Felix Linker <[e-mail]> wrote:
>
> Hi Nadim,
>
> Thanks for putting in the work and bringing some bugs to our attention!
>
> I can confirm that with theories 1-3 you identified two bugs. We fixed
> both bugs in these pull requests:
>
>    - https://github.com/tamarin-prover/tamarin-prover/pull/915
>    - https://github.com/tamarin-prover/tamarin-prover/pull/916
>
> Theories 5 and 8 do not exemplify a bug.
>
> As for theories 1 to 2, the issue is that you add a restriction that uses
> the last keyword. That keyword is intended for internal use only. We didn’t
> check in enough places that this keyword does not occur. It’s debatable
> whether this is a soundness bug as no proof rule was changed. We didn’t
> apply all necessary checks to the input, though.
>
> In theory 3, the property proven true is in fact true. But you are right
> that a warning should be generated to inform the user about the modeling
> mistake.
>
> Theories 5 and 8 are not buggy. To prove "false" lemmas, they require
> using correctly refuted sources or auxiliary lemmas. A lemma can only be
> considered proven when the lemma itself and all auxiliary/sources lemmas
> that it relies upon are proven. This is not the case here. But I and others
> certainly see room for improvement of Tamarin's usability; the issue is
> known to the team:
> https://github.com/tamarin-prover/tamarin-prover/issues/454
>
> Best,
> Felix
>
>
> Am Di., 11. Aug. 2026 um 12:58 Uhr schrieb Nadim Kobeissi
> <[e-mail]>:
>
>> I just found many critical soundness bugs in Tamarin using an LLM.
>> Artifacts as well as paper are here:
>>
>> https://github.com/nadimkobeissi/tamarin-bugs
>>
>> This has been disclosed to the Tamarin developers.
>>
>> (Paper will soon be on ePrint.)
>>
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>>
>> On 29 Jul 2026, at 5:14 PM, Salz, Rich <rsalz=[e-mail]>
>> wrote:
>>
>> I *think*​ this is on-topic for this list, apologies if not (and if you
>> could explain the why I’d greatly appreciate it). From
>> https://infosec.exchange/@0xabad1dea/117002106099986943
>>
>> Someone used an LLM to generate a proof of the Collatz conjecture, and a
>> proof of its correctness from Lean. Turns out bugs in the prover, and
>> related provers, were exploited to show the proof was correct; it wasn’t.
>>
>> Links to all the info are in the URL above.
>>
>> --
>> Ufmrg mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
>>
>>
>> --
>> Ufmrg mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
>>
>
>