COVERT addresses the growing complexity of modern computing architectures by developing formally verified, reusable concurrency abstractions that ensure both safety and security. Targeting multi-processor and concurrent systems, COVERT builds rigorous foundations and practical tools for reasoning about advanced hardware features (e.g., weak memory, speculative execution) and malicious threat models. Its verified litmus tests, concurrency libraries, and mechanised proofs in Isabelle will support secure and performant software across diverse platforms.
Our vision is to provide reusable models, tools and techniques that enable the verification of safety and security properties over a range of advanced architectures, and a verified set of concurrency abstractions that guarantee both safety and security.
We are pleased to announce the official lauch of the COVERT project website!
