The new edition of the SCION Book contains several chapters on the formal verification of the SCION protocol and its implementation
Thibault Dardinier and Jonas Fiala won the first prize at the verifyThis 2022 Competition using Viper. Congratulations!
Marco Eilers defended his thesis Modular Specification and Verifications of Security Properties for Mainstream Languages
Our new verifier 2vyper for Etherium smart contracts written in Vyper won a Distinguished Artifact Award at OOPSLA 2021
We released a new stable version of the Viper verification infrastructure in February 2022
A verified security architecture. More
An automated verifier for Python. More
Formal verification of the SCION internet architecture implementation. More
Formal foundations of translational verifiers. More
An automated, modular verifier for Go. More
A verifier for Rust programs. More
A verification infrastructure for permission-based reasoning. More
