BesFS: Mechanized Proof of an Iago-Safe Filesystem for Enclaves Paper Checout the USENIX Security paper here Source code for BesFS Coq Proof Please refer to the README.md file in the coq folder