The content of the current buffer will be lost.

Try Why3

Type some program in the text area below, then select 'Prove all' in the Why3 menu to generate proof obligations.

Related links