formal-specification
There are 73 repositories under formal-specification topic.
PrincetonUniversity/VST
Verified Software Toolchain
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
Fault-lang/Fault
a language for building system dynamic models
tofgarion/spark-by-example
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
will62794/spectacle
Interactive playground for exploring and sharing TLA+ specifications in the browser.
AdaCore/RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
fraunhoferfokus/acsl-by-example
Public snapshots of "ACSL by Example"
engboris/stellogen
An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax
workcraft/workcraft
Toolset to capture, simulate, synthesize and verify graph models
AllanBlanchard/tutoriel_wp
Frama-C and WP tutorial
GaloisInc/grift
Galois RISC-V ISA Formal Tools
awslabs/aws-lc-verification
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.
ElNiak/awesome-formal-verification
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.
evdenis/verker
Linux kernel library functions formally verified.
SRI-CSL/solidity
This is solc-verify, a modular verifier for Solidity.
ldv-klever/klever
Read-only mirror of the Klever Git repository
paulch42/lean-spec
Program Specification in Lean 4
appliedfm/vstyle
A style guide for Coq
decanus/rutschblock
A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+
agra-uni-bremen/libriscv
Extensible implementation of the RISC-V ISA based on FreeMonads
tomooda/ViennaTalk
ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk
grayswandyr/electrod
Formal analysis for the Electrod formal specification language
postechsv/tee-formal-spec
Formal Specification of Trusted Execution Environment APIs
MasWag/monaa
A Tool for Timed Patten Matching with Automata-Based Acceleration
dgpv/miniscript-alloy-spec
Formal specification for Miniscript in Alloy
radprogrammer/delphi-language-spec
Unofficial, community-driven language specification for the Delphi programming language (Object Pascal) — including lexical rules, grammar, and semantic details.
vacp2p/formalities
Formal models of vac protocols
ZikangXiong/diff-spec
Differentiable Symbolic Specification
doganulus/reelay-codegen
A code generator from high-level formal specifications for monitoring and pattern matching sequential/temporal data.
Inferara/inference-language-spec
🌀 Inference programming language specification
vladstejeroiu/Dafny-programs
Examples of formal verifications written in Dafny.
ElNiak/Toward-verification-of-QUIC-extensions
Formal methods play an important role in validating networking protocols. During the development of TLS 1.3, formal methods have helped to identify several issues with draft versions of the protocol that have been fixed before finalising the protocol. In the transport layer, the QUIC protocol has been proposed to replace the HTTP/TLS/TCP stack. This protocol is being finalised within the IETF and deployed by Google, Cloudlfare, Facebook and many others.
ShrohanMohapatra/ExplorePLT
A repository that describes my explorations on formal verification using Dafny, techniques from programming language theory such as CYK parsing, Earley parsing, type-theoretic things like lambda calculus etc.
tungminhphan/reactive_contracts
An implementation of a reactive GR(1) contract
tzanis-anevlavis/evrostos
Evrostos: The rLTL Verifier
Inferara/inf-wasm-tools
WASM tools with non deterministic operations support