FSCQ is a certified filesystem written and proven correct in Coq. It&#x27;s the first filesystem with a machine-checkable proof that it&#x27;s implementation meets its specification and whose specification includes crashes.<p>The full source code of FSCQ is available online: <a href="https:&#x2F;&#x2F;github.com&#x2F;mit-pdos&#x2F;fscq-impl" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;mit-pdos&#x2F;fscq-impl</a>