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.

Language: Coq - Size: 578 KB - Last synced: 2 days ago - Pushed: 3 days ago - Stars: 20 - Forks: 15

grayswandyr/electrod

Formal analysis for the Electrod formal specification language

Language: OCaml - Size: 2.35 MB - Last synced: about 4 hours ago - Pushed: about 20 hours ago - Stars: 10 - Forks: 4

AdaCore/RecordFlux

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

Language: Ada - Size: 27.4 MB - Last synced: about 16 hours ago - Pushed: about 21 hours ago - Stars: 101 - Forks: 6

workcraft/workcraft

Toolset to capture, simulate, synthesize and verify graph models

Language: Java - Size: 63.6 MB - Last synced: about 16 hours ago - Pushed: about 18 hours ago - Stars: 55 - Forks: 142

Fault-lang/Fault

a language for building system dynamic models

Language: Go - Size: 26.2 MB - Last synced: 5 days ago - Pushed: 5 days ago - Stars: 163 - Forks: 7

ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced: 9 days ago - Pushed: 12 days ago - Stars: 20 - Forks: 12

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 71.9 MB - Last synced: 16 days ago - Pushed: 21 days ago - Stars: 415 - Forks: 88

somombo/swaps-perm

Formally defines permutations of arrays and proves related theorems

Language: Lean - Size: 12.7 KB - Last synced: 14 days ago - Pushed: 15 days ago - Stars: 2 - Forks: 0

tomooda/ViennaTalk

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

Language: Smalltalk - Size: 45.2 MB - Last synced: 15 days ago - Pushed: 15 days ago - Stars: 14 - Forks: 0

doganulus/reelay-codegen

A code generator from high-level formal specifications for monitoring and pattern matching sequential/temporal data.

Language: Python - Size: 7.87 MB - Last synced: 15 days ago - Pushed: over 4 years ago - Stars: 6 - Forks: 1

LambdaAlpha/airlang_rs

The Air programming language is carefully designed to solve programming problems once and for all.

Language: Rust - Size: 1.36 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 7 - Forks: 0

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced: 25 days ago - Pushed: over 2 years ago - Stars: 15 - Forks: 0

paulch42/lean-spec

Program Specification in Lean 4

Language: Lean - Size: 279 KB - Last synced: 23 days ago - Pushed: 4 months ago - Stars: 11 - Forks: 1

parof/protocol-validation

Language: TeX - Size: 222 KB - Last synced: 30 days ago - Pushed: over 4 years ago - Stars: 2 - Forks: 0

agra-uni-bremen/libriscv

Extensible implementation of the RISC-V ISA based on FreeMonads

Language: Haskell - Size: 301 KB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 4 - Forks: 1

PatrickShaw/University-FIT3013-LiftSystemSpecification

A formal specification written in Event-B notation that formally specifies the behaviour of a multi-lift elevator system.

Size: 790 KB - Last synced: about 1 month ago - Pushed: about 7 years ago - Stars: 2 - Forks: 0

PatrickShaw/University-FIT3013-LiftSystemModel

A model checking specification written in NuSMV that specifies a model of a single lift elevator system.

Language: Batchfile - Size: 261 KB - Last synced: about 1 month ago - Pushed: about 7 years ago - Stars: 0 - Forks: 0

GaloisInc/grift

Galois RISC-V ISA Formal Tools

Language: Haskell - Size: 7.55 MB - Last synced: 8 days ago - Pushed: 4 months ago - Stars: 54 - Forks: 8

ARM-software/asl-interpreter

Example implementation of Arm's Architecture Specification Language (ASL)

Language: OCaml - Size: 82 KB - Last synced: 2 months ago - Pushed: over 4 years ago - Stars: 94 - Forks: 25

hwayne/learntla-v2

Learn TLA+ for free! No prior experience necessary!

Language: TLA - Size: 2.12 MB - Last synced: 2 months ago - Pushed: 3 months ago - Stars: 164 - Forks: 37

ZikangXiong/diff-spec

Differentiable Symbolic Specification

Language: Python - Size: 51.8 KB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 3 - Forks: 1

fraunhoferfokus/acsl-by-example

Public snapshots of "ACSL by Example"

Language: TeX - Size: 20.8 MB - Last synced: about 1 month ago - Pushed: almost 3 years ago - Stars: 94 - Forks: 19

appliedfm/coq-vsu-int63

Formally verified 63-bit integer arithmetic, implemented in C and proven in Coq

Language: Coq - Size: 146 KB - Last synced: 24 days ago - Pushed: about 2 years ago - Stars: 2 - Forks: 0

LambdaAlpha/airlang

The Air programming language is carefully designed to solve programming problems once and for all.

Size: 85 KB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 3 - Forks: 0

evdenis/verker 📦

Linux kernel library functions formally verified.

Language: C - Size: 5.37 MB - Last synced: about 2 months ago - Pushed: over 3 years ago - Stars: 47 - Forks: 7

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

Language: Ada - Size: 1.03 MB - Last synced: 11 days ago - Pushed: over 1 year ago - Stars: 150 - Forks: 16

SRI-CSL/solidity Fork of ethereum/solidity

This is solc-verify, a modular verifier for Solidity.

Language: C++ - Size: 47.2 MB - Last synced: 4 days ago - Pushed: 8 months ago - Stars: 51 - Forks: 14

AllanBlanchard/tutoriel_wp

Frama-C and WP tutorial

Language: TeX - Size: 9.81 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 41 - Forks: 16

smtifahim/EFBO-Ontology-Repository

This repository contains three ontology files relevant to the Event-Based Functional Behaviour Ontology (EFBO) project as part of a Software Engineering thesis.

Language: HTML - Size: 280 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

agra-uni-bremen/formal-iss

Generate an ISS for riscv-vp from a formal LibRISCV ISA model

Language: Haskell - Size: 47.9 KB - Last synced: about 2 months ago - Pushed: 10 months ago - Stars: 1 - Forks: 1

kooixh/rewrite-system

My third year University dissertation, Term Rewriting System

Language: Java - Size: 825 KB - Last synced: 7 months ago - Pushed: over 3 years ago - Stars: 0 - Forks: 0

Isaac-DeFrain/bft-specs

TLA+ specifications for BFT algorithms

Language: TLA - Size: 17.6 KB - Last synced: 4 months ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

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.

Language: Python - Size: 7.84 MB - Last synced: 8 months ago - Pushed: almost 3 years ago - Stars: 4 - Forks: 0

Bo-Yuan-Huang/lmac-ila

ILA of LMAC

Language: C++ - Size: 92.8 KB - Last synced: 8 months ago - Pushed: almost 5 years ago - Stars: 0 - Forks: 1

cristian404dev/deterministic-finite-automaton

Deterministic finite automaton in Java

Language: Java - Size: 56.6 KB - Last synced: 8 months ago - Pushed: over 3 years ago - Stars: 1 - Forks: 0

raymonddeng99/PlusCal

TLA+ verification of some distributed protocols

Language: TLA - Size: 1000 Bytes - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

eltonvs/uno-b

A formally specified UNO game using B-Method

Language: C - Size: 34.2 KB - Last synced: 9 months ago - Pushed: almost 6 years ago - Stars: 2 - Forks: 0

tomooda/ViennaVM

a simple virtual machine for VDM by VDM

Language: C - Size: 177 KB - Last synced: 9 months ago - Pushed: almost 4 years ago - Stars: 0 - Forks: 0

tomooda/VDM-benchmark

a collection of benchmarks for VDM-SL interpreters/code generators

Size: 8.79 KB - Last synced: 9 months ago - Pushed: almost 4 years ago - Stars: 0 - Forks: 0

tomooda/pyVDMC

VDM-SL execution library using public/private VDMPad servers.

Language: Python - Size: 168 KB - Last synced: 9 months ago - Pushed: almost 9 years ago - Stars: 2 - Forks: 0

cister-labs/fvoca2223

Web page hosting the pedagocical material prepared in the scope of the FVOCA class of the MESCC MSc

Language: HTML - Size: 2.11 MB - Last synced: 10 months ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

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.

Size: 3.39 GB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 1 - Forks: 1

decanus/rutschblock

A TLA+ implementation of the Avalanche Protocol Family, both for learning Avalanche and TLA+

Language: TLA - Size: 21.5 KB - Last synced: 30 days ago - Pushed: about 4 years ago - Stars: 18 - Forks: 1

dgpv/miniscript-alloy-spec

Formal specification for Miniscript in Alloy

Language: Alloy - Size: 163 KB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 9 - Forks: 5

nicholasRenninger/autonomousCarControlSynthesis

LTL to Control Synthesis (using formal methods concepts) Framework for a Basic Highway Driving Scenario

Language: Python - Size: 1.71 MB - Last synced: about 1 year ago - Pushed: almost 5 years ago - Stars: 0 - Forks: 0

vladstejeroiu/Dafny-programs

Examples of formal verifications written in Dafny.

Language: Dafny - Size: 93.8 KB - Last synced: about 1 year ago - Pushed: about 3 years ago - Stars: 2 - Forks: 2

arcadio/ajcontract

Design by contract extension to Java using annotations and bytecode injection

Language: Java - Size: 20.5 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 1 - Forks: 0

MasWag/monaa

A Tool for Timed Patten Matching with Automata-Based Acceleration

Language: C++ - Size: 2.06 MB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 8 - Forks: 0

isabelleysseric/Synchronisation_feux_circulation

Specification and formal verification of traffic light control system.

Language: Java - Size: 9.35 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0

joulook/Formal-Specification-and-Verification-of-Programs-Fall-2020

In this repository you can find all of my assignments for Formal Specification and Verification of Programs Course when I was in 1st semester of my master's at SUT.

Language: TeX - Size: 5.13 MB - Last synced: 6 months ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0

ggzor/specifying-verifying-tail-recursion

Source code for the paper "Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions"

Language: TeX - Size: 2.5 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 1

codeanonorg/Octo-syn

Shellcode synthesizer

Language: OCaml - Size: 28.3 KB - Last synced: 12 months ago - Pushed: over 3 years ago - Stars: 3 - Forks: 0

appliedfm/coq-vsu

Tools for working with Verified Software Units

Language: OCaml - Size: 36.1 KB - Last synced: 25 days ago - Pushed: over 2 years ago - Stars: 1 - Forks: 0

tzanis-anevlavis/evrostos

Evrostos: The rLTL Verifier

Language: C - Size: 10.8 MB - Last synced: about 2 months ago - Pushed: over 2 years ago - Stars: 3 - Forks: 1

reity/article-specifications-for-distinguishing-functions

This article presents a technique for assembling concise, lightweight specifications and unit tests for verifying the identity of a function; the technique sacrifices completeness to enable compact and portable specifications.

Language: Jupyter Notebook - Size: 13.7 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0

tungminhphan/reactive_contracts

An implementation of a reactive GR(1) contract

Language: Python - Size: 15.9 MB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 3 - Forks: 0

vacp2p/formalities

Formal models of vac protocols

Language: TLA - Size: 40 KB - Last synced: about 1 year ago - Pushed: about 4 years ago - Stars: 7 - Forks: 4

tomooda/VCParser

A little combinatory parser in VDM-SL

Size: 43 KB - Last synced: 9 months ago - Pushed: almost 4 years ago - Stars: 0 - Forks: 0

robkorn/mCRL2-spacemacs-layer

Integration of the mCRL2 toolset into Spacemacs with Syntax highlighting.

Language: Emacs Lisp - Size: 6.84 KB - Last synced: about 1 year ago - Pushed: about 5 years ago - Stars: 0 - Forks: 0

tomooda/JSONUtil

JSON parser/printer for VDM-SL

Size: 125 KB - Last synced: 9 months ago - Pushed: over 10 years ago - Stars: 0 - Forks: 0

azmanuddin94/FormalMethod

Formal specification for student class written in VDM++

Size: 1000 Bytes - Last synced: about 1 year ago - Pushed: over 6 years ago - Stars: 0 - Forks: 0