magmide
Verification engine
Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers.
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
810 stars
51 watching
13 forks
Language: Coq
last commit: over 2 years agocoqdependent-typesformal-methodsformal-verificationlogicsystems-programmingtype-safetyverification
Related projects:
| Repository | Description | Stars |
|---|---|---|
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 70 |
| imdea-software/fcsl-pcm | A formalisation of Partial Commutative Monoids (PCMs) for verification of concurrent programs. | 26 |
 logsem/aneris | A framework for developing and verifying distributed systems using separation logic | 33 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 verifytests/verify.moq | Adds Verify support for Moq types to verify mock behavior and assertions | 14 |
 wasmcert/wasmcert-coq | A formalisation of WebAssembly in Coq to provide proof of correctness and type safety for its programming model. | 100 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 143 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
| mit-plv/kami | A platform for high-level parametric hardware specification and modular verification | 143 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 220 |
 sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 21 |
 mmcco/verified-parser-example | A formally verified parser implementation using Coq and OCaml | 20 |