james/bq
Watch
1
0
Fork
You've already forked bq
 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
A Lean 4 model of the BQ batching queue with a machine checked proof of safety (https://gibsonsec.net/~karlsson/bq.pdf) https://gibsonsec.net/~karlsson/bq.pdf
1 commit 1 branch 0 tags 6.4 MiB
  • Lean 82.8%
  • TeX 9.7%
  • Python 7.5%
Find a file
Exact
Repository files (latest commit first)
Filename Latest commit message Latest commit date
james 4465add2ae initial commit
2026-09-25 19:00:34 +00:00
BQ initial commit 2026-09-25 19:00:34 +00:00
diagrams initial commit 2026-09-25 19:00:34 +00:00
docs initial commit 2026-09-25 19:00:34 +00:00
paper initial commit 2026-09-25 19:00:34 +00:00
.gitignore initial commit 2026-09-25 19:00:34 +00:00
BQ.lean initial commit 2026-09-25 19:00:34 +00:00
lake-manifest.json initial commit 2026-09-25 19:00:34 +00:00
lakefile.toml initial commit 2026-09-25 19:00:34 +00:00
lean-toolchain initial commit 2026-09-25 19:00:34 +00:00
Main.lean initial commit 2026-09-25 19:00:34 +00:00
README.md initial commit 2026-09-25 19:00:34 +00:00

README.md