Introducing
Introducing Gobstopper
Gobstopper stubs out stale tool output in Claude Code and Codex sessions by a rule you set, after archiving the original so you can search it or restore it.
Blog
Posts about Gobstopper: what it does, how its archive and edit limits are checked, and what those checks leave out.
Technique
How Gobstopper proves its compaction arithmetic and transcript laws
Gobstopper uses Kani to check its edit limits and token sums for every value of their numeric inputs, and Lean to prove that masking keeps each record's ID, order, and tool links.
Published
Technique
How Gobstopper checks its archive against crashes at every step
Gobstopper model-checks its archive design with a crash allowed at every step, and each safety rule has a broken copy that must reproduce the loss it prevents.
Published