Having tried one of the earliest versions of Verifpal last year, as a beginner to those tools, going from Tamarin to Verifpal was going from “unusable” to “easy”. Analysis speed was a big part of that, but so was the syntax and semantics of the protocol description language.
Still haven’t gotten around to it, but I consider Verifpal a mandatory gateway to version 1.0 of Monokex (a Noise ripoff I’m working on that Nadim audited), or even any new protocol I dare invent.
Verifpal provides formal methods to the masses. We had TLA+ in a similar vein before for concurrent programs. I can’t wait to see other domains have similar tools.
Thanks very much Loup, looking forward to checking out your coming work.
I think that especially when I see comments like this, I’m glad that I wrote this post. The second part explains clearly the differences in what Verifpal can guarantee versus a more comprehensive tool like Tamarin, and outlines that the ease of use does come at a slight cost in rigor and complete proofyness (I wonder if I just coined that term).
Having tried one of the earliest versions of Verifpal last year, as a beginner to those tools, going from Tamarin to Verifpal was going from “unusable” to “easy”. Analysis speed was a big part of that, but so was the syntax and semantics of the protocol description language.
Still haven’t gotten around to it, but I consider Verifpal a mandatory gateway to version 1.0 of Monokex (a Noise ripoff I’m working on that Nadim audited), or even any new protocol I dare invent.
Verifpal provides formal methods to the masses. We had TLA+ in a similar vein before for concurrent programs. I can’t wait to see other domains have similar tools.
Thanks very much Loup, looking forward to checking out your coming work.
I think that especially when I see comments like this, I’m glad that I wrote this post. The second part explains clearly the differences in what Verifpal can guarantee versus a more comprehensive tool like Tamarin, and outlines that the ease of use does come at a slight cost in rigor and complete proofyness (I wonder if I just coined that term).