Proof of Go 1.23's sync.Map
- Rocq Prover 95%
- Go 4.3%
- Verilog 0.3%
- Dafny 0.2%
- Makefile 0.1%
- Other 0.1%
| .devcontainer | ||
| .vscode | ||
| dafny | ||
| etc | ||
| go | ||
| perennial@f17fe1dedf | ||
| src | ||
| .gitignore | ||
| .gitmodules | ||
| _CoqProject | ||
| Makefile | ||
| README.md | ||
Systems verification sync.Map proof
This repo has the setup for verifying the Go 1.23 standard library sync.Map.
It was derived from the proof assignment repo for CS 839: Systems verification, taught at UW-Madison in Fall 2025 by Tej Chajed.
Once you have Rocq installed, build the provided code by running make.
The goose translation of this code has some bugs related to generics: they have been fixed after translation with this sed command:
./etc/update-goose.sh
gsed -i 's/#\(entry\|Map\)/\1/g' src/code/sys_verif_code/go_sync_map.v