Skip to content

@mit-pdos MIT PDOS

All

    Repositories list

    61 repositories

    • perennial

      Public
      Verifying concurrent storage and distributed systems
      concurrencyverificationrocq
      concurrencyverificationrocq
      Lean
      •53•246•18•7•Updated Oct 12, 2026Oct 12, 2026

    • 6.1600-notes

      Public
      TeX
      •
      Other
      •4•8•0•3•Updated Oct 11, 2026Oct 11, 2026

    • security-book

      Public
      TeX
      •
      Other
      •4•3•0•0•Updated Oct 11, 2026Oct 11, 2026

    • xv6iris

      Public
      Lean
      •2•36•1•0•Updated Oct 9, 2026Oct 9, 2026

    • xv6-riscv

      Public
      Xv6 for RISC-V
      C
      •
      Other
      •4.4k•11k•0•3•Updated Oct 9, 2026Oct 9, 2026

    • 6.1600-labs

      Public
      Student lab assignments for MIT 6.1600
      Python
      •18•13•0•0•Updated Oct 7, 2026Oct 7, 2026

    • tulip

      Public
      Go
      •
      MIT License
      •0•4•0•0•Updated Sep 29, 2026Sep 29, 2026

    • tulip-proof

      Public
      Verification of tulip
      Rocq Prover
      •
      MIT License
      •0•2•0•0•Updated Sep 29, 2026Sep 29, 2026

    • xv6-riscv-book

      Public
      Text describing xv6 on RISC-V
      TeX
      •
      Other
      •217•981•4•2•Updated Sep 23, 2026Sep 23, 2026

    • sigmaos

      Public
      Go
      •
      MIT License
      •22•166•2•5•Updated Aug 10, 2026Aug 10, 2026

    • xv6-book

      Public
      Commentary for xv6-public
      Perl
      •
      Other
      •67•278•8•13•Updated Aug 6, 2026Aug 6, 2026

    • perennial-cli

      Public
      Tool to manage perennial verification projects
      Go
      •
      MIT License
      •2•4•0•4•Updated Jul 20, 2026Jul 20, 2026

    • gokv

      Public
      Go
      •5•17•0•0•Updated Apr 6, 2026Apr 6, 2026

    • argosy

      Public
      Proving crash safety for systems with layered recovery
      coqverificationrecovery
      coqverificationrecovery
      Rocq Prover
      •
      MIT License
      •8•16•0•0•Updated Apr 1, 2026Apr 1, 2026

    • 6.566-lab-2026

      Public
      Python
      •
      Other
      •1•0•0•0•Updated Mar 31, 2026Mar 31, 2026

    • gojournal-proof

      Public
      Verification of GoJournal
      Rocq Prover
      •
      MIT License
      •0•3•0•0•Updated Dec 9, 2025Dec 9, 2025

    • grove-proofs

      Public
      Proofs of distributed systems using Grove
      Rocq Prover
      •
      MIT License
      •0•3•0•0•Updated Dec 7, 2025Dec 7, 2025

    • go-liveness

      Public
      Go
      •0•0•0•0•Updated Sep 5, 2025Sep 5, 2025

    • vmvcc

      Public
      Go
      •
      MIT License
      •4•30•0•0•Updated May 8, 2025May 8, 2025

    • DeathStarBench

      Public
      Open-source benchmark suite for cloud microservices
      C
      •
      Apache License 2.0
      •514•3•0•0•Updated Oct 28, 2024Oct 28, 2024

    • daisy-nfsd

      Public
      DaisyNFS is an NFS server verified using Dafny and Perennial.
      verificationdafny
      verificationdafny
      Dafny
      •
      MIT License
      •6•43•0•0•Updated Oct 16, 2024Oct 16, 2024

    • xv6-public

      Public
      xv6 OS
      C
      •
      Other
      •4.6k•9.7k•1•79•Updated Aug 13, 2024Aug 13, 2024

    • go-nfsd

      Public
      Fast NFS server implemented using GoJournal
      Go
      •
      MIT License
      •2•54•1•0•Updated Jul 20, 2024Jul 20, 2024

    • go-journal

      Public
      Verified, concurrent, crash-safe transaction system
      verification
      verification
      Go
      •
      MIT License
      •6•62•1•2•Updated Jul 20, 2024Jul 20, 2024

    • perennial-examples

      Public
      Examples verified using Perennial
      Go
      •
      MIT License
      •0•5•0•0•Updated Jul 20, 2024Jul 20, 2024

    • 6.566-lab-2024

      Public
      Python
      •
      Other
      •10•8•0•0•Updated May 2, 2024May 2, 2024

    • 6.828-qemu

      Public
      qemu patched for debugging, used for 6.828
      C
      •
      Other
      •62•85•2•1•Updated Mar 10, 2024Mar 10, 2024

    • grove

      Public
      Experiments in verifying distributed systems with Iris
      0•2•0•0•Updated Oct 24, 2023Oct 24, 2023

    • grove-artifact

      Public
      Python
      •1•3•0•0•Updated Aug 11, 2023Aug 11, 2023

    • go-ycsb

      Public
      Fork of https://github.com/pingcap/go-ycsb/ with support for benchmarking GroveKV.
      Go
      •
      Apache License 2.0
      •0•0•0•0•Updated Jul 25, 2023Jul 25, 2023
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.