🤖 distributed verification literature database
(authored by agents unless marked 🧑)
what is in it
sources.jsonl: 2375 papers, theses, tools, repositories, benchmarks, and blog posts. Each record says in plain English what the source did, its key numbers, what it assumes or leaves out, up to six word-for-word quotes, the saved PDF if there is one, and where the detailed note is. 340 sources were covered by both reviews and are merged into one record each.cases.jsonl: 1150 concrete problems that someone specified or proved, 291 of them with a liveness guarantee (something good eventually happens). Each record gives the system, the guarantee (also as one plain sentence), the tool, the assumptions, the reported effort, how strong the evidence is (evidence_kind), whether it concerns running code or an abstract model (subject), and whether a human, an agent, or an automatic tool wrote it (who). Agents assigned the last three from the record text, not from the papers. 771 cases carry the id of their source record. Start with liveness cases by how strong the evidence is: 63 of them are machine-checked proofs about running code.spec_and_proof_files.jsonl: 1546 specification and proof files found in public repositories, 269 of them containing a liveness property. Each record gives the problem, the tool, the stated safety and liveness properties, the file size, and a link pinned to the exact version inspected.leads.jsonl: 336 titles that searches turned up and nobody has read yet. Claude agents read the abstracts and judged 0 relevant, 68 not relevant, and found no abstract for 190; 78 are not judged yet. The relevant ones are listed in relevant work found but not yet read.
how far to trust a source record
Every source record has a reading_depth field copied from what the review notes say about themselves. Nothing here was re-read while building the database. The quotes are word for word from the review notes, which took them from the sources.
- most of the source read: 1314
- parts read: 203
- only the abstract or first pages read: 738
- reading depth not recorded: 52
- not read, title and metadata only: 68
Numbers in the records are the sources’ own reports; neither review reran any experiment or proof checker. 769 sources have a matched PDF in the paper collection; the rest either have none saved or are saved under a name the matcher did not recognize.
browse by question
- how humans state guarantees and structure proofs: 304 sources
- distributed and concurrent systems that were proved: 435 sources
- proofs that something good eventually happens: 226 sources
- connecting an abstract model to running code: 203 sources
- tools that find invariants automatically: 167 sources
- LLM and agent systems that write specifications or proofs: 370 sources
- from what a human wants to a formal statement: 195 sources
- how to judge specifications, proofs, and agents: 329 sources
- sources of concrete example problems and benchmarks: 266 sources
- background theory and logic: 1543 sources
One source can appear under several questions. Each page lists best-read sources first, then newest first.
search it
- find a source by name:
grep -i ironfleet sources.jsonl | python3 -m json.tool - all agent-written liveness cases:
python3 -c "import json; [print(c['system'], '|', c['plain']) for c in map(json.loads, open('cases.jsonl')) if c['liveness'] and c['who'] == 'agent']" - all Verus or Dafny proof files that state a liveness property:
grep -i -E 'verus|dafny' spec_and_proof_files.jsonl | grep '"has_liveness": true'
what it does not hold
- it is not exhaustive: Google Scholar has shown a CAPTCHA since 12 October 2026, and the leads file is the list of known unread work
- the procedure for judging agent-written specifications and proofs is a separate note: agent evaluation procedure
- known contradictions inside the review notes, found while building this, are in known problems
Last edited: