A verification toolchain for Rust programs

ACL2 System and Books as Maintained by the Community

Read-only mirror of the Klever Git repository

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

Our Official Blog: we write about the development of EOLANG and 𝜑-calculus

Interface with the rustc compiler for the purpose of program verification

The P programming language.

Open tool platform for the cost effective rigorous development of dependable complex software systems services. This platform is based on the Event-B formal method and provides natural support for refinement and mathematical proof.

Creusot helps you prove your code is correct in an automated fashion.

HACL*, a formally verified cryptographic library written in F*

A human-friendly and developer-friendly math proof assistant

Learn TLA+ for free! No prior experience necessary!

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.

Verified Software Toolchain

Formal analysis for the Electrod formal specification language

ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.

Verification framework and tool for higher-order Scala programs