why3 开源项目推荐（16 个）

creusot-rs /creusot

Creusot帮助您证明您的Rust代码是正确的。

lengyijun /tarjan-kosaraju-why3-lean4

该项目在 GitHub 上没有填写描述

evdenis /acsl-skills

Agent Skills for deductive verification of C with Frama-C/WP: writing ACSL specifications, running and triaging proofs, designing provable C, and hand-written Coq when nothing else closes the goal.

orlandopalmeira /Trabalhos-MFES-2023-2024

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)

hyperpolymath /bactrian

Research-stage verification suite for a pure OCaml subset, BEAM actor protocols, and Idris2/Zig FFI boundaries. Targets Why3/SMT, Apalache, and checked proof receipts. Current contents are architecture, an implementation roadmap, and fail-closed readiness tooling; the proof engine is not yet implemented.

hyperpolymath /Apodeixis.jl

Research-stage Julia verification toolchain for contracts, compiler analysis, numeric semantics, and verified FFI with independently checked proof targets.

al-alawi-deterministic-theorem /hcsp-sovereign-semiconductor-formal-verification-matrix

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.

JGalego /highlightjs-why3

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

al-alawi-deterministic-theorem /HCSP-Sovereign-Kernel-Formal-Verification

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.

al-alawi-deterministic-theorem /-Alalawi-Deterministic-Sovereign-Core-ADSC-HCSP-

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

MMarchand-NSI /why3

Ongoing work for proving correctness using why3

danielevardito /MSM

Metadata Snippet Manager - CLI version

Cactus-proj /whymp

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/

Tillerino /docker-why3

Docker image for the why3 system with some preinstalled provers

kmneumann /Why3-A-Star

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

Cactus-proj /why3

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