fscq
File system
A file system written and verified in the Coq proof assistant with a focus on security.
FSCQ is a certified file system written and proven in Coq
237 stars
38 watching
21 forks
Language: Coq
last commit: almost 4 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
| mit-pdos/perennial | A system for verifying correctness of concurrent and crash-safe systems with recovery procedures | 165 |
 mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 110 |
 heades/system-f-coq | An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 mhogomchungu/sirikali | A Qt/C++ GUI front end to various encrypted file systems and SSHFS | 785 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 jscoq/jscoq | An online development environment for the proof assistant Coq, allowing users to run and interact with it in their browser. | 518 |
 snu-sf/paco | A Coq library for proving properties about stateful systems through parameterized coinduction | 43 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
 ms-jpq/sad | A CLI tool that uses fzf and diff for interactive search, replace, and review of changes in text files before committing them. | 1,799 |
 sifive/prockami | Formal verification and implementation of RISC-V processor designs using Coq. | 22 |
 thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |