Formal Verification

2025/26

In this course, we cover classical software verification techniques—both automatic and interactive—supported by the use of two verification tools: Rocq and Why3.

This course unit begins with an introduction to the Rocq Prover and the underlying type system. The Rocq Prover combines higher-order logic with a richly typed functional language. It supports defining data structures and functions, stating theorems and specifications, interactively developing and machine-checking proofs, and extracting certified programs to other languages. It is a very mature tool that has seen numerous applications across different domains. High-profile success stories include the mechanized proof of the Four Color Theorem and the full formal certification of the CompCert C compiler, both landmark results in formal methods.

In the second part of this course unit, we will explore the Why3 verifier, already introduced in MFES (in the context of deductive verification of sequential imperative algorithms and functional algorithms), now applied to the specification and verification of non-sequential algorithms, namely concurrent, self-stabilizing, and distributed algorithms.

Syllabus

• Computer-assisted theorem proving with the Rocq Prover
  • …
• Specification and verification of non-sequential algorithms with Why3
  • …

Teaching Team

• Maria João Frade (MJF)
• Jorge Sousa Pinto (JSP)

Assessment

• Continuous assessment with two evaluation components:
  • Laboratory test on the Rocq prover (50%)
  • Individual written test on deductive verification with Why3 (50%)
• The exam will have the two parts with the same weightings

Timetable

Type	Time	Room
Lecture / Teórica	Wen/4ªf. 9h-10h	Ed.7 1.09
Tuturial / Pratica-Lab	Wen/4ªf. 10h-12h	Ed.7 1.09

Planning

#	Date	Instructor	Summary
1	11 Fev	MJF	Type-theoretic notions for proof-checking. Rocq in brief.
2	18 Fev	MJF	Deductive reasoning in Rocq.
3	25 Fev	MJF	Inductive reasoning in Rocq.
4	4 Mar	MJF	Programming and Proving in Rocq.
5	11 Mar	MJF	Case study in Rocq.
6	18 Mar	MJF	Test (Rocq)
7	25 Mar	JSP	Deductive verification of transition systems in Why3.
8	8 Apr	JSP	Deductive verification of concurrent algorithms in Why3.
9	15 Apr	JSP	Deductive verification of token-based mutual exclusion algorithms in Why3.
10	22 Apr	JSP	Deductive verification of message-passing distributed algorithms in Why3.
11	29 Apr	JSP	Refinement of transition systems in Why3.
12	6 May	JSP	Test (Why3)
	???	MJF+JSP	Exam

Material

Lecture Slides

• A very brief introduction to the Rocq Prover and its foundations

Lecture Examples

• lesson1.v

Exercises

• Rocq(1).pdf

Bibliography

• The Rocq Documentation
• The Why3 Platform François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Andrei Paskevich. Version 1.8, September 2025

Further reading

• Yves Bertot. Coq in a Hurry. INRIA 2017.
• Software Foundations Series
• …

Tools

• The Rocq Prover
• Why3 - Where Programs Meet Provers