Skip to content
master
Switch branches/tags
Go to file
Code

Latest commit

No proof, but a (hopefully) correct implementation.

Fixes issue #15.
19b13f4

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
src
 
 
xv6
 
 
 
 
 
 
 
 

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.

About

FSCQ is a certified file system written and proven in Coq

Resources

License

Releases

No releases published

Packages

No packages published