[Verifpal] Congratulations on the 0.2 release!

[Nadim Kobeissi]

Thank you Michiel; hello everyone, and welcome to the Verifpal Mailing List.

I’m very pleased that Verifpal is now available for everyone, and hope to receive feedback from the community over the coming days and weeks so that the project can evolve. Let me share some starting notes on what I expect in the coming weeks:

1. TRYING OUT VERIFPAL
The first step will be having the community discover what the heck Verifpal is. You can do so by checking out the Verifpal User Manual and the software itself here:
https://verifpal.com/#download
Try evaluating some of the existing models in the `examples` directly, and write your own!

2. QUESTIONS, SUGGESTIONS, DISCUSSIONS
I’ve already seen some cool discussions and questions from folks online, and I’ve encouraged them to instead submit these questions here on the Verifpal Mailing List so we can have a unified body of knowledge of the community’s discussions moving forward. Then, bug fixes! Features! Hopefully we’ll make some progress there.
Don’t forget that Verifpal is governed by the Community Guidelines:
https://github.com/SymbolicSoft/verifpal/blob/master/CONTRIBUTING.md

3. VERIFPAL IN THE CLASSROOM
A major target of Verifpal is the undergraduate computer science classroom. My fall semester at NYU begins next Monday, September 2nd, and I’ll be using the Verifpal User Manual as a textbook for a large chunk of my course. I very much look forward to writing an email here on my experiences doing so, and whether Verifpal succeeds in teaching formal verification in the undergraduate setting, something that appears to currently not be realistically achievable by other tools.

4. PLANNED MAJOR FEATURES:
a. Finishing a soundness proof on Verifpal’s verification methodology.
b. Generating prototype implementations in Golang of Verifpal models.
c. Launching “VerifHub”, an online hub where people can post and discuss protocol models!
d. Improving the Visual Studio Code extension such that verification results pop up directly inside the VSCode IDE.

5. THANK YOU, NLNET
Another warm thanks to Michiel and to NLNet, which was as responsible as I am in making Verifpal exist. Their support for Verifpal was indispensable, and I am committed to pushing it forward as a harbinger for a new era in accessible formal verification for all enthusiasts, students and engineers!

ALSO: STICKERS
In less important but still cool & fun news, there is also now an official Verifpal Sticker Shop!
https://verifpal.com/stickers

Thanks, everyone!

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Aug 27, 2019, at 2:10 PM, Michiel Leenaars via Verifpal <verifpal at lists.symbolic.software> wrote:
> 
> Hello all,
> 
> Nadim has made the first public release of VerifPal today. sooner than expected. Brilliant work without a shadow of a doubt, and very user-friendly indeed!
> 
> I am very curious what people will do with this now it is out there. It has a low barrier to entry, which makes it a technology commons that can make symbolic formal verification far more widely accessible than has so far been the case - contributing to a safer and more secure internet for all. Looking very much forward to future work, building on top of VerifPal.
> 
> Best,
> Michiel Leenaars
> NLnet Foundation
> 
> P.S. If you have a great idea like this, you might consider asking a grant from the Next Generation Internet initiative too via https://nlnet.nl/PET
> 
> 
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal