mit-pdos / Fscq
Licence: other
FSCQ is a certified file system written and proven in Coq
Projects that are alternatives of or similar to Fscq
GeocoqA formalization of geometry in Coq based on Tarski's axiom system
Stars: ✭ 128 (-38.46%)
Mutual labels: coq
VscoqA Visual Studio Code extension for Coq [[email protected],@fakusb]
Stars: ✭ 138 (-33.65%)
Mutual labels: coq
Coq Chick Blog🐣 A blog engine written and proven in Coq
Stars: ✭ 173 (-16.83%)
Mutual labels: coq
InteractiontreesA Library for Representing Recursive and Impure Programs in Coq
Stars: ✭ 133 (-36.06%)
Mutual labels: coq
Advent Of Coq 2018Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
Stars: ✭ 137 (-34.13%)
Mutual labels: coq
CoqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Stars: ✭ 157 (-24.52%)
Mutual labels: coq
Coq Of OcamlImport OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-43.75%)
Mutual labels: coq
MetacoqMetaprogramming in Coq
Stars: ✭ 192 (-7.69%)
Mutual labels: coq
Bedrock2A work-in-progress language and compiler for verified low-level programming
Stars: ✭ 138 (-33.65%)
Mutual labels: coq
Fpga readingsRecipe for FPGA cooking
Stars: ✭ 164 (-21.15%)
Mutual labels: coq
Math ClassesA library of abstract interfaces for mathematical structures in Coq [[email protected]]
Stars: ✭ 133 (-36.06%)
Mutual labels: coq
Coq HaskellA library for formalizing Haskell types and functions in Coq
Stars: ✭ 135 (-35.1%)
Mutual labels: coq
KamiKami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
Stars: ✭ 158 (-24.04%)
Mutual labels: coq
Dotformalization of the Dependent Object Types (DOT) calculus
Stars: ✭ 132 (-36.54%)
Mutual labels: coq
JscertA Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
Stars: ✭ 186 (-10.58%)
Mutual labels: coq
FiatMostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-42.79%)
Mutual labels: coq
Verdi RaftAn implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Stars: ✭ 143 (-31.25%)
Mutual labels: coq
CoqgymA Learning Environment for Theorem Proving with the Coq proof assistant
Stars: ✭ 201 (-3.37%)
Mutual labels: coq
QuickchickRandomized Property-Based Testing Plugin for Coq
Stars: ✭ 188 (-9.62%)
Mutual labels: coq
Coq EquationsA function definition package for Coq
Stars: ✭ 158 (-24.04%)
Mutual labels: coq
FSCQ
FSCQ is a file system written and verified in the Coq proof assistant.
Unmaintained research prototype
Warning: the FSCQ software is not maintained. FSCQ's core is verified in
Coq, but FSCQ also includes components written in Haskell for interacting
with FUSE, and depends on FUSE and Haskell bindings for FUSE, none of
which are verified. The unverified portions are likely to have bugs,
and we do not recommend that anyone use the FSCQ research prototype
in practice.
Although the overall software is not maintained, we would be interested
in hearing from others that discover issues with the verified portions
of FSCQ.
Branches
There are several branches in this repository, corresponding to different
FSCQ-related projects.
-
The master branch contains the source code for the DFSCQ file system,
roughly corresponding to the SOSP 2017 paper.
-
The security branch contains the source code for the SFSCQ file
system and the DiskSec sealed block framework, roughly corresponding to
the OSDI 2018 paper.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at
[email protected].
