Creusot helps you prove your Rust code is correct.
Repositório dos trabalhos de casa da UC de Métodos Formais em Engenharia de Software (MFES) - Mestrado em Engenharia Informática (MEI/MIEI) - Universidade do Minho (UMinho)
A FORK: WhyMP is an arbitrary-precision integer library for C that is inspired by GMP, implemented in WhyML, and formally verified using Why3. https://gitlab.inria.fr/why3/whymp/
"A mathematically-verified deterministic core acting as a security filter. Fully proved (19/19 obligations) via Frama-C (Alt-Ergo/Why3), Coq, TAL+, and LTL.
A highlight.js language grammar for Why3, a platform for deductive program verification
The 10/10 formal verification matrix for the HCSP architecture using Frama-C, AstraVer, Coq, and TLA+ to mathematically eliminate memory corruption and zero-day exploits at Ring 0.
Unofficial mirror of Wyh3: https://gitlab.inria.fr/why3/why3/
Repository containing code for the paper: "Why3 and Proving A* Automatically"
Official TLA+ specifications and Why3 formal verification artifacts for the HCSP Sovereign Deterministic Core, proving 100% complete logic correctness (19/19 goals) against zero-day exploits and cloud-freezing deadlocks.
Add a description, image, and links to the why3 topic page so that developers can more easily learn about it.
To associate your repository with the why3 topic, visit your repo's landing page and select "manage topics."