Verified Software Toolchain
Learn TLA+ for free! No prior experience necessary!
Interactive playground for exploring and sharing TLA+ specifications in the browser.
Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.
a language for building system dynamic models
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
An experimental language exploring computation and meaning through term unification, with logic-agnostic types.
Public snapshots of "ACSL by Example"
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Frama-C and WP tutorial
Toolset to capture, simulate, synthesize and verify graph models
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.
Linux kernel library functions formally verified.
Galois RISC-V ISA Formal Tools
This is solc-verify, a modular verifier for Solidity.
AI-Native Formal Specification Language — a bounded model checker (Lark + Z3) built for LLM write/verify/repair loops.
Read-only mirror of the Klever Git repository
Program Specification in Lean 4
🌀 Inference programming language
Formal specification of Resonate, written in Lean 4
To associate your repository with the formal-specification topic, visit your repo's landing page and select "manage topics."