Skip to content


  • Pro


@mit-pdos @coq-community


  1. Tricks you wish the Coq manual told you

    Coq 236 8

  2. Ltac2 tutorial

    Coq 17

  3. Goose converts a small subset of Go to Coq

    Go 21 1

  4. Verifying concurrent crash-safe systems

    Coq 37 8

  5. FSCQ is a certified file system written and proven in Coq

    Coq 198 17

  6. Library to create Coq record update functions

    Coq 18 2

2,288 contributions in the last year

Jul Aug Sep Oct Nov Dec Jan Feb Mar Apr May Jun Mon Wed Fri

Contribution activity

July 2020

Created a pull request in mit-pdos/perennial that received 5 comments

Remove later in definition of na_crash_inv

This is an incomparable definition; it's weaker in that allocating a crash invariant now requires proving persistently(Q -* P) now instead of later…

+14 −14 5 comments

Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.