This list is things that I'd like to verify, or that might be easily verifiable. I'd like to keep the list open-source, and for now it's all C because that's what I'm thinking about, but other contributions and suggestions are more than welcome via PR, email or Twitter!
Right now I've written this with SAW in mind, because that's where my focus is. If other languages/tools show up, it's probably worth adding a column.
Finally, if you're interested in actually doing some verification, please reach out. An important part of what we're workign on now is trying out our tools, and we'd gladly offer some mentoring time to any willing or aspiring victims proof engineers.
| Project | Notes | Suggester (thanks!) |
|---|---|---|
| Wasm3 | Link | Frank |
| LibSodium | optimized x86! | DKP |
| Sweet-B | need to examine this code | Brian Mastenbrook |
| Signal C implementation | Matthew Fernandez, Aaron Tomb | |
| DTach | Pretty small and self-contained, any obvious properties? | Tikhon Jelvis |
| ASN.1 | So many bugs, so much code | Martin Nyx Brain |
| Azure C SDK | Memory safety targets, api stuff is harder | Me |
| Compression/Image libraries | Probably lots to do, binary formats would be fun. Some specs are very clear | Tristan Ravitch |
| Curl | So much here, probably some high impact parts | Tom DuBuisson |
| libflint | Tom DuBuisson | |
| sudo (parsing) | Tom DuBuisson |
Funny suggestions that fill me with rage or fear (nonexclusive or). Honestly all of these are probably chock-full of bugs and good problems. We'll know we've won the verification game when we can move them up to the "real list".
| Project | Notes | Suggester (no thanks!) |
|---|---|---|
| Doom (memory allocater) | Bugs might be useful for speedrunners. Seriously there's probably good targets in here, but I'm too scared | Dominic Orchard |
| GMP | Yeah, I'm going to verify a program I can't draw a smiley face in. | Sebastian Ullrich |
| Red/Black Tree | We're going to need a bigger boat (and a separation logic) | Martin Nyx Brain |