Creusot helps you prove your Rust code is correct.

Language for program verification using Hoare logic

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)

Docker image for the why3 system with some preinstalled provers

"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.

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.

Metadata Snippet Manager - CLI version

why3 basic verified dpll sat solver (homework lmao)

A highlight.js language grammar for Why3, a platform for deductive program verification

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/

Ongoing work for proving correctness using why3

Repository containing code for the paper: "Why3 and Proving A* Automatically"

Unofficial mirror of Wyh3: https://gitlab.inria.fr/why3/why3/

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.