StainlessVerification framework and tool for higher-order Scala programs
Acl2ACL2 System and Books as Maintained by the Community
Spark By ExampleSPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
Hacl StarHACL*, a formally verified cryptographic library written in F*
ScallinaA Coq-based synthesis of Scala programs which are correct-by-construction
CosaCoreIR Symbolic Analyzer
MathlibLean mathematical components library
OakMeaningful control of data in distributed systems.
Sledthe champagne of beta embedded databases
Practical FmA gently curated list of companies using verification formal methods in industry
z-evesZ-EVES for linux. Probably the only place you can find it
z3 tutorialJupyter notebooks for tutorial on the Z3 SMT solver
fm-notesUnassorted scribbles on formal methods, type theory, category theory, and so on, and so on
TSNschedAutomated Schedule Generation for Time-Sensitive Networks (TSN).
high-assurance-legacyLegacy code connected to the high-assurance implementation of the Ouroboros protocol family
tlacliA script for running TLA+/TLC from the command line
kleverRead-only mirror of the Klever Git repository
koikaA core language for rule-based hardware design 🦑
mSATA modular sat/smt solver with proof output.