FreeSpecA framework for implementing and certifying impure computations in Coq
RiscvSpecFormalThe RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
tezedge-specificationTLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus
avrReads a state transition system and performs property checking
fm-notesUnassorted scribbles on formal methods, type theory, category theory, and so on, and so on
high-assurance-legacyLegacy code connected to the high-assurance implementation of the Ouroboros protocol family
gammaAn Eclipse-based modeling framework for the component-based design and analysis of reactive systems
pldi19-equivalence-checkerSource code for the equivalence checker presented in the PLDI 2019 paper, "Semantic Program Alignment for Equivalence Checking"
awesome-rust-formalized-reasoningAn exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
acsl-provedFully proved small C functions (examples for verification course).
kleverRead-only mirror of the Klever Git repository