GitXplorerGitXplorer
m

fscq

public
234 stars
20 forks
5 issues

Commits

List of commits on branch master.
Verified
2c7ef9c268fd79a81b26b44ef720f8e6a1e938a0

Merge pull request #18 from Armael/ocaml_extraction

zzeldovich committed 2 years ago
Unverified
4ee8310e9ccadd17ca0f3f7c36ddb0a1aa14baae

Makefile: update wrt ocaml extraction

AArmael committed 2 years ago
Unverified
587c44c1f7d97b6672ebf28227db27d48df81dbf

Refresh the OCaml extraction

AArmael committed 2 years ago
Verified
30c9c48f5494fa872d95e4fc5fc0f2098582fccc

Merge pull request #17 from Armael/fixproofs813

zzeldovich committed 2 years ago
Unverified
c89edacd00e21f350f341c24154e362d3599e280

Repair proofs

AArmael committed 2 years ago
Unverified
35dcb8eaf068ae9c106154a8dd160bf78f5a76b4

Update build instructions

ttchajed committed 3 years ago

README

The README file for this repository.

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.