Verified Software Toolchain
Learn TLA+ for free! No prior experience necessary!
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
Example implementation of Arm's Architecture Specification Language (ASL)
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Public snapshots of "ACSL by Example"
Toolset to capture, simulate, synthesize and verify graph models
Galois RISC-V ISA Formal Tools
Frama-C and WP tutorial
This is solc-verify, a modular verifier for Solidity.
Linux kernel library functions formally verified.
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.
Read-only mirror of the Klever Git repository
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
A style guide for Coq
ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk
Formal analysis for the Electrod formal specification language
Program Specification in Lean 4
The Air programming language is carefully designed to solve programming problems once and for all.
Add a description, image, and links to the formal-specification topic page so that developers can more easily learn about it.
To associate your repository with the formal-specification topic, visit your repo's landing page and select "manage topics."