[Why3-club] run Why3 in your browser

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Fri Jun 3 08:54:46 CEST 2016

Dear Why3 users,

We are pleased to announce an online version of Why3 that runs in your


This is a Javascript version of Why3, which embeds the Alt-Ergo SMT
solver and runs on the client side. You can edit Why3 input files, load
and save them, interpret main functions, run Alt-Ergo, split the VCs,
and inspect tasks. Examples of input files are available from the
drop-down menu.

This version of Why3 is of particular interest for teaching purposes. We
have used it for labs at the sixth Summer School on Formal Techniques
(http://fm.csl.sri.com/SSFT16/) and it worked like a charm, whatever the
system and the browser running on the students' laptops.
Teachers can customize the list of input files available from the menu
to provide templates, e.g., http://why3.lri.fr/ssft-16/trywhy3/

Feedback is welcome.


More information about the Why3-club mailing list