🤖 database, connecting an abstract model to running code

(authored by agents unless marked 🧑)

203 sources, best-read first, then newest first. Generated from sources.jsonl; edit the reviews’ notes, not this page.

• Can Code Specify a System Precisely Enough to Formally Verify It? (2026)
  • what: Audits a deployed restaurant point-of-sale payment workflow (register, payment terminal, Finix backend). The authors built TLA+ models with Claude agents under their supervision. They also compared LLMs generating specifications from the TypeScript source in three forms: library-based JavaScript, a bare JavaScript next-function, and TLA+.
  • number: pre-fix models have 43-103 states, check in under a second, counterexamples 6-9 steps
  • number: 7 original gaps found, 3 reproduced on the unmodified code with its emulator
  • number: final failure-enabled model has 376 distinct states; 24-hunk patch; passes all 23 scenario tests
  • number: 105 generations (7 models x 3 contracts x 5), each replayed on 101 observed transition windows
  • limits: Every checked property is a safety invariant (a fact true in every reachable state) on finite, simplified models, not on all executions of the TypeScript. Timeout liveness is not checked. The model and the emulator shared a wrong reading of how Finix responds to a duplicate key. There is no mechanical proof that code matches model. Crashes and power loss remain accepted risks.
  • how much was read: most of it read
  • source; notes: Can Code Specify a System Precisely Enough to Formally Verify It?; notes: Can Code Specify a System Precisely Enough to Formally Verify It?
  • record id: can-code-specify-a-2026
• CircuitProver (2026)
  • title: CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
  • what: Introduces CircuitProver, a Lean 4 framework that translates parameterized Chisel hardware and natural-language specifications into Lean, uses an agent to iteratively construct machine-checked proofs, and distills proof trajectories into reusable guidance and theorem libraries. The deterministic Chisel-to-Lean translator preserves parameters, interfaces, registers and width-aware bitvector transitions; small-width co-simulation checks the translation. Agents formulate Lean specifications, build hardware-aware scaffolds, prove one-step/invariant lemmas, and repair scripts using Lean feedback. Two libraries separate reusable proof plans from module-independent checked theorems. The carry-skip-adder case extracts a block recurrence, full-width radix closure and targeted representation repair. The 63-task suite spans arithmetic/control/memory/miscellaneous designs plus XiangShan/Rocket arithmetic modules, with ablations isolating guidance and theorem-library effects and model-scaling comparisons.
  • number: 63 benchmark tasks: 34 arithmetic, 9 control, 9 memory, 11 miscellaneous
  • number: 63/63 CircuitProver; 58/63 vanilla; 31/63 Chicala/Stainless
  • number: 50.0% fewer proof rounds
  • number: 23.2% lower verification time
  • limits: The frontend supports only a subset of Chisel and generated Lean models are validated by exhaustive small-bit-width co-simulation, not all parameter widths. Success requires a final Lean file with no sorry/admit/axiom/unsafe. Cost averages are over solved tasks, so comparisons have different coverage. Results use Claude agents and a benchmark authored by the researchers; industrial RTL, richer properties and broader designs remain future work. Natural-language specification formalization still requires semantic agent reasoning.
  • how much was read: most of it read
  • record id: circuitprover-2026
• EqiVM (2026)
  • title: Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens (EqiVM)
  • what: Agents write Lean proofs that deployed Ethereum contract bytecode refines (correctly implements) a spec written in the authors’ Sol- language. The proofs use a formal semantics of the EVM. The agent is an untrusted proof producer, so its proofs are checked.
  • number: text says 19 contracts proved complete, abstract says 23, conclusion says 27 (notes’ own count: 27)
  • number: Vat: 6,965 bytecode bytes, 556 spec lines, 84,382 Lean proof lines, 100h44m, 2 effective human prompts, 74.8M fresh tokens, about $1,380retrospectiveAPIprice-number:Cat:106.8Mtokens,64h,17prompts-number:Clipper26/29functionsafter81h44m;NounsAuction18/20after94h28mwithcertificatechecktimingout-limits:Itdoesnotshowtransactionavailability,boundedgas,eventualcompletionorsoundnessofthesuppliedpolicy.Therefinementrelationpermitsvacuitythroughgasexhaustion(runningoutofgasmakesaclaimholdtrivially).ThetrustedbaseincludestheEVMformalization,importedLeanaxiomsandnativ{e}_{d}ecide.Ahumansuppliesthehigh-levelspec.-howmuchwasread:mostofitread-[source](https://arxiv.org/abs/2607.26306v1);[notes:FoundationalRefinementProofsforDeployedBytecode,atthePriceof](../distribute{d}_{v}erificatio{n}_{r}evie{w}_b/dee{p}_1{1}_{s}econ{d}_{p}as{s}_{a}gent{s}_{i}nvariants.md);[notes:FoundationalRefinementProofsforDeployedBytecode,atthePriceof](../distribute{d}_{v}erificatio{n}_{r}evie{w}_b/dee{p}_1{4}_{p}rogra{m}_{a}gents.md)-recordid:‘eqivm-2026‘-ESBMC-Arduinohardware-faithfulPLCverification(2026)-title:ESBMC-Arduino:ClosingtheDeploymentGapforFormalVerificationofOpen-HardwarePLCs-what:Introducesahardware-faithfulverificationmethodforIEC61131-3programsonopen-hardwarePLCsandinstantiatesitasESBMC-Arduino.AdeclarativeHALfixesMCUwordwidth,ADC/PWMresolutionsandI/Obindings;theloweringinjectsrealizableinputboundsandbit-precisearithmeticbeforeESBMCBMC/k-induction.Thepaperformalizesthedeploymentgapasdisagreementbetweenanabstractmodelwithunboundedintegers/freeinputsandadevicemodelwithfinite-widtharithmeticandhardwaredomains.ItdefinesHALH=<w,badc,bpwm,mu>,givesfourloweringtransformations(width,inputassumes,quantization/PWMclamp,nondeterministicnonlinearabstraction),andprovesReac{h}_{d}evicesubsetReac{h}_{m}odelunderafaithfuldescriptor,witheveryreportedcounterexamplephysicallyrealizable.Themotivatingadc\ast 100alarmflipsatAVRadc=898.Controlledvariantsisolatevulnerablescalingversussafeoffsets/comparisons.The123-programcorpusfinds54/123naivefalsealarms,allunphysicalIN-5underflows;HALboundsreduce54to0whileretaining32proofs.CBMCandFrama-Cmirrorsreproducethephantomandgenuinewidthdefect.-number:123realprograms;naive54unsafe,37unknown,32safe-number:HALannotated:0unsafe,91unknown,32safe;all54falsealarmsremoved-number:Controlledmediansolvetime168ms,maximum412ms;realrunsunder1s-number:CBMCreproduces54/54naiveoverflowsandboundsremove54/54-limits:Scopeisinteger/BooleanIEClogicandmodel-levelverification,nothardware-in-loop.Scan-cyclesamplingignoresplantdynamics,sensornoiseandactuatorlatency.SoundnessdependsoncorrectHALwordwidthandper-inputranges;uniform10-bitAVRtreatmentcanbewrongforwiderADC,networkordigital-wordinputs.Nonlinearblocksaresoundbutimprecisenondeterministicranges,andk-inductionleaves91realprogramsunknown.Bindingandquantizationmechanismsarefuturework.-howmuchwasread:mostofitread--recordid:‘esbmc-arduino-hardware-faithful-plc-verification-2026‘-Fairneris(2026)-title:AHigher-OrderSeparationLogicforVerifyingLiveness-PreservingRefinementsofDistributedSystems-what:AlogicmechanizedinRocq.IttransfersprogressofamodeltoprogressofanAnerisLangimplementation,assumingafairschedulerandafairnetwork.Thenetworkmaydrop,duplicateandreordermessages.Fairnesshereappliestosetsofmessages.-number:two-nodeimplementation;everysequencenumbereventuallygetsareplyassumingcallbackterminationandfairness-number:noLOC,person-timeorbenchmarktimingreported-limits:Itverifiescodeunderthelanguag{e}^{\prime }sownoperationalsemantics,notaproductionRustorOCamlexecutable.Humanssupplythemodel,invariants,contractsandrefinementproofs.TheURLofthemechanizationartifactisnotgiven.-howmuchwasread:mostofitread-[source](https://hal.science/hal-05647709v1/document);[notes:AHigher-OrderSeparationLogicforVerifyingLiveness-PreservingRefi](../distribute{d}_{v}erificatio{n}_{r}evie{w}_b/dee{p}_1{0}_{s}econ{d}_{p}as{s}_{l}ivenes{s}_{p}roofs.md)-recordid:‘fairneris-2026‘-FederatedFormalVerification(2026)-title:FederatedFormalVerification:Cross-BackendCitation,Cross-AxisConvergence,andAI-OrchestratedProofDispatchforProductionSystems-what:ThisworksendstheopenTLA+proofobligationsofaproductionRaftsystemtoCoq,Lean,Why3,Apalache,Z3andCBMC.ClaudeCodespecialistshandleeachbackend.CIrecheckstheproofs,andthesystemgeneratesJavaruntimeassertions.-number:17activehours,263commits,26-axiomcensusclosed-number:abouttwentyspecialistagentsinfourwavesof3/6/7/4;practicalconcurrency6-7-number:prooftreeover11,000lines,18apexobligations-number:Coq8/8passes,median34.4s;Apalache0/3;TLC0/5;PRISM1/13-limits:Ahumanwrotetheclaimthatthebackendsareequivalent.ThereisnoartifactURL.Thepapergivesnoprompts,nocost,andnobreakdownofhumaneffort.TheJavaassertionscheckteststatesonly,notrefinement.Thespeedupcomparesdifferentprotocols.ApalacherefutedapropertythatCoqcited,atboundsix.-howmuchwasread:mostofitread-[source](https://arxiv.org/abs/2606.02019);[notes:FederatedFormalVerification:Cross-BackendCitation,Cross-AxisConv](../distribute{d}_{v}erificatio{n}_{r}evie{w}_b/dee{p}_1{1}_{s}econ{d}_{p}as{s}_{a}gent{s}_{i}nvariants.md)-recordid:‘federated-formal-verification-2026‘-HarnessLLM(2026)-title:HarnessLLM:RustVerificationHarnessGenerationwithLargeLanguageModels-what:AnLLMworkflowturnsaRustprojec{t}^{\prime }sexistingunittestsintoharnesses(smalldriverprogramswithsymbolicinputs)fortheKaniboundedmodelchecker.Itfindsthecallpatternsintests,buildssymbolicargumentsfortheprojec{t}^{\prime }sowntypesbyfollowingconstructors,andrepairscompileerrorswithoutlettingtheLLMinventtypes.-number:9Rustcrates,494tests,6651linesoftestcode:294callingscenariosextracted,94.66-number:294of294harnessescompileinKaniwithin10attempts;97.3-number:Average145sand$0.03 per harness (GPT-4.1)
  • number: Kani Autoharness baseline produced harnesses for 41% of the same scenarios
  • limits: Needs a codebase with good tests; sparse tests lower scenario coverage. ‘Success’ means the harness compiles in Kani, not that it checks anything beyond memory safety and panics. Bounded checking; the LLM picks the bounds (slice lengths, unwind). Only functions visible in source (macro-generated ones are missed).
  • how much was read: most of it read
  • source; notes: HarnessLLM (2026)
  • record id: harnessllm-2026
• ICEPICK API model checking (2026)
  • title: Systematic API Testing Through Model Checking and Executable Contracts
  • what: Introduces ICEPICK, a black-box REST API testing framework that models API state in TLA+, exhaustively explores the TLC state-space graph, extracts call sequences, and checks execution with GLACIER first-order contracts. The paper specifies a two-phase pipeline: CRUD/OAS contract generation, manual semantic predicates, a conservative TLA+ abstraction, TLC state-space preprocessing, coverage-guided BFS path selection, and execution with an emulator that evaluates preconditions, postconditions and invariants. PUT updates are inserted into post/delete paths; results are classified OK, WARN, ERR or NOT_TESTED. State coverage is complete for generated paths, while transition coverage can miss parallel transitions represented by the same abstract state pair. In the evaluation, Tournaments, Petstore and Features-Service expose distinct scalability and compliance behavior; injected delete and referential-integrity faults are detected, but non-REST APIs block useful inference.
  • number: 17 SSG configurations
  • number: 30–99.4% SSG size reduction after preprocessing
  • number: 5–21 GB models complete within about an hour
  • number: 467 GB and 16 h 16 min for Tournaments size 12
  • limits: The approach requires resource-oriented REST APIs, accurate schemas and HTTP status semantics; generated contracts are intentionally partial and domain invariants may require manual predicates. TLA+ models are abstractions that can diverge from implementations. TLC and path extraction face state explosion: on the reported hardware about 5–21 GB SSGs finish within an hour, while a 467 GB model takes 16 h 16 min; a 100 GB heap handled about 46K states/349K transitions. Only three systems were evaluated, and three-value configurations produced infeasible request counts.
  • how much was read: most of it read
  • record id: icepick-api-model-checking-2026
• IDS (2026)
  • title: Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
  • what: Given a specification written by an expert in Rocq/Coq, a coordinator of GPT-5.4 workers writes an implementation and a proof that Coq’s kernel checks. It can throw away a data representation and start over. Code is extracted to OCaml.
  • number: Seven distributed key-value specifications succeed (at least 2 of 3 runs); 20/21 runs (notes’ arithmetic)
  • number: 6.8 hours and 106 per spec - number: Plain Codex and Claude Code each solve 2/7 - number: Artifacts from 622 to 3,924 lines of code plus proof, 25-128 lemmas - limits: The specification is supplied. Safety holds only within the supplied model, and there is no liveness. The comparison of human effort is not a controlled experiment. - how much was read: most of it read - source; notes: IDS: changing code and abstractions makes otherwise hard proofs tracta - record id: `ids-2026` - JS-SAM (2026) - title: Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench - what: This controlled study compares LLMs writing JavaScript (SAM) specs against TLA+ specs of real systems. The authors check the specs by bounded exploration, plus replay against traces captured from the running systems. - number: 4 models, 5 generations per cell - number: Spin traces: 28 windows, 8 of 18 observable input combinations covered - number: small tasks 40/40 complete passes; Raft scale 0/20 initially, 6/20 after one repair round - number: state-changing conformance of original models ranges 0-86.4% though all pass syntax and invariants - limits: It checks no liveness or temporal properties. It explores only to a bound. It does not prove that the implementation matches the model. The author designed the instrumentation, the reference model and the prompts. - how much was read: most of it read - source; notes: JS-SAM: a controlled case study separating specification shape from la; notes: JS-SAM: a controlled case study separating specification shape from la - record id: `js-sam-2026` - k8s-runtime-audit (2026) - title: Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking - what: A TLA+ model of a tenant-isolation policy is replayed over Kubernetes audit logs. The logs travel through a webhook and NATS JetStream to a customized TLC. It flags cross-tenant access, dangling bindings and cluster-admin bindings. - number: 5 controlled scenarios, all detected - number: one control-plane and two worker nodes; 10/50/100/1000 actions, 2/5/10 tenants - number: batch cap 50 messages, 4.5 s pull expiration - number: 2 tenants, 1000 actions: 1071.20 messages, 24.5 ± 0.8 ms per message; 10 tenants: 689.60, 70.3 ± 1.7 ms - limits: It checks recorded traces. It does not prove the implementation or the spec correct. It relies on logs that are complete and in order. The model omits namespace-local Roles. It has no liveness. No size or hours are given. - how much was read: most of it read - source; notes: Monitoring and Verification of Multitenant Kubernetes Clusters using T - record id: `k8s-runtime-audit-2026` - LeaseGuard (2026) - title: LeaseGuard: Raft Leases Done Right - what: LeaseGuard is a Raft lease design. A new leader can accept writes at once, and can serve reads that the old leader's writes do not affect, from the log it inherited. The authors built a TLA+ model, a Python simulator and a LogCabin C++ implementation. - number: TLA+ bounds: 3 servers, 2 keys, term 3, log length 4, clock 8, lease 3; 296-line model - number: about 1,000 simulator lines; 1,600 server and 650 client lines changed in 27,000-line C++ code - number: writes about 1000 to 10,000 per second - number: failover: 9,930 of 10,000 reads succeeded in the wait - limits: The safety argument is a paper sketch, not machine-checked. The TLA+ model checks safety only to a bound, with no temporal properties. There is no agent workflow. An earlier model hid the bug inside large atomic actions. - how much was read: most of it read - source; notes: Related-work addition: LeaseGuard: Raft Leases Done Right - record id: `leaseguard-2026` - Neuro-formal verification (2026) - title: Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning - what: Proposes NFV: an AI agent translates mainstream-language source, property and environment assumptions into staged formal artifacts, then uses Dafny or CBMC to produce machine-checked proofs/refutations. Goal-blind stages (formalize model, property and environment separately before proof search) reduce proving a mismatched artifact, while admitting formalization itself is not soundly guaranteed. The pipeline distinguishes verification and refutation arms, performs artifact audits and abstains when formalization/type checks fail. A balanced nl2post-safe corpus has 206 program/spec pairs (103 correct, 103 mutants), with library tiers L0–L3. Dafny handles proof/refutation; CBMC translates libraries to C for bounded counterexamples. Error analysis attributes wrong verdicts to missing or stronger preconditions and library formalization. - number: 206 entries: 103 correct + 103 buggy - number: Dafny pipeline issued 128 verdicts, 10 wrong: 92.2% precision, 57.3% recall, F1 0.71 - number: Dafny verification 72/103 correct (93.5% precision); refutation 47/103 buggy (88.7% precision) - number: CBMC refuted 65/103 buggy, 7 false: 63% recall, 90% precision - limits: NFV optimizes empirical accuracy rather than end-to-end soundness because informal environment assumptions cannot be fully guaranteed. Results assume docstrings capture intended properties; unstated preconditions caused all six false refutations. Dafny modeling of libraries and Python semantics is incomplete; CBMC is bounded and checks C translation rather than original Python. - how much was read: most of it read - source - record id: `neuro-formal-verification-2026` - Perennial issue 638 (2026) - title: Goose and Go-semantics defects found on master - what: The issue reports translator and Go-semantics defects found while verifying etcd v3.7.2 and raft with Goose, with before/after tests and fixes proposed. - number: 11 translator defects and 10 Rocq Go-semantics problems are listed. - limits: Open issue; branch master/lean applicability is still being coordinated. - how much was read: most of it read - source - record id: `perennial-issue-638-2026` - Perennial proof tutorial (2026) - title: Perennial Proof Tutorial (Lean) - what: The tutorial explains how to write Lean proofs for Go code in Perennial and says tutorial snippets are checked from a canonical Lean file. - limits: Tutorial verification was not rerun. - how much was read: most of it read - source - record id: `perennial-proof-tutorial-2026` - PRDT (2026) - title: PRDTs: Composable Design and Verification of Consensus Protocols using Replicated Data Types - what: Scala components for replicated state with decisions. Two local obligations are enough for consensus safety, and Stainless checks them. Paxos-style compositions and a key-value store are built from the components. - number: verification obligations reduced from four to two - number: key-value store compared with etcd in one- and three-region setups; leader-failure experiment at 10 s with 5 s timeout - number: no proof size, runtime or person-hours reported - number: Paper reports verified implementations of multiple Paxos-family protocols - limits: Covers the safety of the executable protocol logic only. No theorem that requests eventually get a response. Networking and storage are not proved. An artifact was promised but not found. - how much was read: most of it read - source; notes: PRDTs: Composable Design and Verification of Consensus Protocols using - record id: `prdt-2026` - Proofs Promptly (2026) - title: Proofs Promptly: An Experience Report on Proof-Oriented Programming with AI Agents - what: The report uses Copilot CLI with Opus 4.5, with skills, subagents and a REPL. It writes Pulse/F* separation-logic proofs of concurrent locks and semaphores, the MSQuic receive buffer, and a port of the OCaml garbage collector. - number: Table 1 p. 3: 1 week/1229, 1 week/$583,2weeks/$1580; about a month and 3,392 total (notes' addition) - number: Six-month manual estimate is the authors' estimate, not a controlled comparison - number: manual proof-engineering cost estimated at roughly half a year - number: three experts, two weeks, versus about half a year manually (authors' estimate) - limits: Experts review the specs and supply the invariants that decide the proof. It has no theorem about distributed fairness or eventual progress. - how much was read: most of it read - source; notes: Proof-oriented programming at Microsoft; notes: papers - record id: `proofs-promptly-2026` - Qoreo (2026) - title: Qoreo: Choreographic Programming for Quantum Distributed Systems - what: Introduces Qoreo, a choreographic language for quantum distributed protocols combining local quantum computation, classical/quantum communication and linear typing, with endpoint projection to node processes. The paper proves local and choreographic type safety, endpoint-projection soundness and completeness, and deadlock freedom for well-typed projected networks. A Rocq mechanization and NetQASM extraction pipeline support simulation/deployment, with QKD-style examples and a runtime API. - number: Metatheory in Sections 3–5 is fully formalized in Rocq - number: Extraction emits Python/NetQASM processes for each participant - number: No quantitative performance benchmark is reported - limits: Deadlock-freedom and projection guarantees require well-typed/projectable choreographies and stated communication restrictions; not every choreography is projectable. The paper’s future work includes knowledge of choice and larger protocol families; extracted execution depends on NetQASM runtime/platform support. - how much was read: most of it read - - record id: `qoreo-2026` - SoK consensus (2026) - title: Systematization of Knowledge: Formal Verification of Consensus Protocols - what: A survey that sorts consensus verification into model checking, deductive proofs, code proofs and hybrids. - number: over 20 verified consensus protocols - number: only about 30% of surveyed works address liveness - number: Matrix covers 20+ protocols in abstract and over 30 in conclusion - number: Only ≈30% of surveyed works address liveness (§5) - limits: It gives no search date range and no count of how many papers were considered, so the reported fraction is not an unbiased census. Table 1 entries need checking against the cited papers. - how much was read: most of it read - source; notes: Systematization of Knowledge: Formal Verification of Consensus Protoco - record id: `sok-consensus-2026` - SpecTrum consensus differential fuzzing (2026) - title: SpecTrum: Specification-Guided Differential Fuzzing for Ethereum Consensus Clients - what: Presents SpecTrum, which mechanizes Ethereum consensus-spec with explicit if-premises, measures premise coverage, and generates inputs from under-exercised premise constraints before running them across five consensus clients. It found 27 cross-client divergence cases, 22 requiring inserted premises. The framework traces input provenance through Consensus-SpecTec, targets false-side premise coverage, mutates fork-aware values, and attributes divergences to six root-cause categories. It validates the mechanized specification against official tests, compares against random/unguided mutation, measures code coverage and implicit-condition gains, and reproduces cases across protocol forks. - number: Validated Consensus-SpecTec against 910 official tests: 581 state-transition and 329 unit tests (§1) - number: Identified 27 cross-client divergences; 22 cannot be found without inserted premises (§1) - number: Premise coverage rose from 46.3% to 91.1%; 151 uncovered conditions were identified and 81 inserted (§1) - number: All 27 divergences reproduced across fork versions (§1) - limits: The approach depends on consensus-spec/SpecTec modeling fidelity, executable client interfaces, and chosen spectest seeds. Premise coverage targets explicit validity conditions and can miss issues outside the mechanized specification. Reported divergences await bug-bounty triage; fork transfer is evaluated for the studied clients and versions. - how much was read: most of it read - - record id: `spectrum-consensus-differential-fuzzing-2026` - Specula (2026) - title: Specula: Scaling formal specifications for autonomous model checking of system code - what: Specula writes TLA+ models and properties from system source code. It checks observed traces against the model and repairs disagreements. It then model checks for violations and tries to reproduce each one in the real code. - number: 48 open-source systems; 249 reproduced bugs; 89 reported to maintainers; 68 confirmed and 24 fixed in that subset - number: only 0.90% of generated properties are liveness; 99.10% safety - number: 200 bugs via model checking, 49 during code reading/modeling - number: median 3.69 hours and 57 per system across 48 systems (§5.3)
  • limits: Model checking plus reproduction gives concrete failures, not proofs for all executions. Its coverage of liveness is weak. The results pool several versions, and only 14 systems used the latest version.
  • how much was read: most of it read
  • source; notes: Specula: close the model–code loop before calling a violation a bug
  • record id: specula-2026
• SysMoBench (2026)
  • title: SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems
  • what: A benchmark of eleven concurrent and distributed systems. An AI writes a TLA+ model of each. The model is scored on syntax, execution, behavioral match to the code, and expected properties.
  • number: source sizes from 175 lines (PGo dqueue) to 5,360 (ZooKeeper leader election)
  • number: Etcd Raft with basic Sonnet agent: 7.69% conformance, 69.23% invariant correctness, 100% syntax
  • number: liveness properties violated 41.9% vs safety 8.3% (§5, Figure 4c)
  • number: each agent run five times, best output evaluated, at most three repairs
  • limits: Covers only the finite executions and configurations supplied. A model can match buggy code and still fail the desired guarantee. The evaluator uses an LLM for some mappings.
  • how much was read: most of it read
  • source; notes: SysMoBench
  • record id: sysmobench-2026
• TLA-Verus (2026)
  • title: TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents
  • what: This work translates existing TLA+ models into Verus temporal proof tasks. The translator is either an algorithm or an LLM writer plus reviewer. It builds on Anvil’s temporal logic library, and agents prove the tasks. Checks freeze the task and reject new assumptions or admissions (unproved claims accepted as true).
  • number: 16,459 model/property pairs attempted
  • number: algorithmic: 5,160 usable translations, 3,094 proofs (304 liveness)
  • number: agentic: 12,352 usable translations, 492 proofs in a 500-task sample
  • number: evaluation: 40 paired tasks, ten per category, 32 models from 24 repositories
  • limits: Showing that the implementation refines the model is future work, so a model proof is not a proof about Rust behavior. An LLM reviews whether the translation is faithful, and this is not proved. The dataset and pipeline are unreleased. The runs were not repeated. A Raft-style model was safe only because it could not make progress.
  • how much was read: most of it read
  • source; notes: closest related work; notes: reported results and populations
  • record id: tla-verus-2026
• TraceFix (2026)
  • title: TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples
  • what: Claude Opus 4.6 turns a task description into a topology of agents, locks and channels. It writes PlusCal for each agent, runs TLC, and repairs from failures. The checked processes become runtime prompts.
  • number: 48 of 48 tasks reach TLC verification; 30/48 pass first try; hard tasks 4/16 first try
  • number: 29 repair attempts: 20 deadlocks, 5 timeouts, 3 syntax errors, 1 undrained channel
  • number: Mean about 594 s and about 4.33 per task - number: 48 tasks, 16 scenario families, all fully TLC-verified; 62.5% first attempt; none over four repairs - limits: Progress is not checked. Repairs for timeouts can reduce fidelity. The runtime monitor checks the topology, not the order of steps. A bounded model-checking pass does not prove that real agents terminate. - how much was read: most of it read - source; notes: TraceFix: generated PlusCal coordination protocols, with important lim - record id: `tracefix-2026` - Velvet (2026) - title: Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean - what: Embeds imperative programs and contracts in Lean. Verification conditions are generated automatically. When automation fails, it leaves ordinary Lean goals, and humans or AI tactics finish them. - number: On average 3.3x fewer total lines than Dafny on manually verified case studies (Section 4, pp. 9-11) - number: 27 VERINA benchmarks; 618 non-comment LOC - number: 21 automatic, 6 manual - number: 3.67x slower than Dafny; all under 45 s - limits: The evaluation is manual verification, not an LLM benchmark. No evidence that agents succeed more often. - how much was read: most of it read - source; notes: Loom/Velvet paper and technical boundary - record id: `velvet-2026` - Verified Romanov Triplet Logic (2026) - title: Formal verification of Romanov’s triplet logic: A verified filter for sliding-window 3-CNF with application to structured formulas - what: Mechanizes Romanov’s Triplet Logic in Rocq, verifies translation/clearing/SVI operations, and extracts a verified filter plus exponential post-check for well-formed sliding-window 3-CNF. The work identifies a precise correctness boundary: SVI is a sound one-sided filter in general, while aligned intersection and a strong CTF predicate restore completeness for the structured sliding-window fragment. The VFR prototype combines machine-checked polynomial filter stages with post-check search and validates outputs against SAT/brute-force oracles. - number: Rocq development exceeds 23,000 lines across 17 files, with 424 proved lemmas/theorems and zero admitted goals - number: 100% agreement with brute-force oracle on random sliding-window instances for n≤6 - number: Polynomial filter stages plus exponential post-check; verified permutation search practical only for n≤8 - limits: Completeness is restricted to well-formed sliding-window/grouped structures; weak CTF can be incomplete and clearing can destroy valid paths. The CNF-to-CTF grouped-window translation remains unverified, post-check is exponential, and verified permutation search is practical only up to n≤8. General 3-SAT still needs external verified solvers/certificates. - how much was read: most of it read - - record id: `verified-romanov-triplet-logic-2026` - Verus-TLA repository (2026) - title: verus-tla export (BasisResearch/verus PR #51) - what: This crate embeds TLA temporal predicates in Verus and provides state-machine structures, fairness predicates and verified helper lemmas for safety and liveness proofs. - number: 8 states - limits: README-level documentation; no independent proof audit was run. - how much was read: most of it read - source; notes: R02. Verus temporal libraries, 2025–2026 repository leads - record id: `verus-tla-repository-2026` - Welder (2026) - title: Welder: Compositional Liveness Verification of Cluster Control Planes - what: Welder proves, for each controller, that it makes progress and limits its requests. This statement is called the CORE spec. It then combines the proofs of controllers that fit together. The authors verified the ReplicaSet, Deployment, StatefulSet and RabbitMQ controllers. - number: 1.5 person-years - number: proof lines: CORE 37,487 (ESR 36,215); executable 3,180; model 3,915; trusted 1,081; about seven minutes to check - number: analysis of 188 reported controller bugs claims CORE excludes 178 (95%) - number: seven bugs found during verification; zero in 629 functional, 1,302 controller-crash, 677 Pod-crash tests - limits: Features left out of the success condition are not checked. The proofs assume that faults eventually stop. Controllers that depend on each other in a circle need separate reasoning. Four controllers lack full feature parity with the upstream versions. The evidence on AI is qualitative only. - how much was read: most of it read - source; notes: Welder: Compositional Liveness Verification of Cluster Control Planes; notes: P07. Welder: Compositional Liveness Verification of Cluster Control Pl - record id: `welder-2026` - AutoMan (2025) - title: AutoMan: Facilitating Verified Distributed Systems Development Through Automatic Code Generation and Manual Optimizations - what: AutoMan generates Dafny implementation code and proof obligations from a protocol specification. The generated code is checked separately. Hand-optimized code may replace generated code if it meets the obligations showing that the implementation matches the spec. The cases are Multi-Paxos from IronFleet, PBFT, a sharded key-value store, and CausalMesh. - number: Multi-Paxos: 2,119 generated lines, about 200 manual annotation lines, about 4 person-hours; optimized version +2,200 lines, about one person-week; IronRSL needed about 8,100 lines - number: KV store: about 80 manual lines in about 2 hours, plus about 1,100 lines and 3 person-days; IronKV 2,700 lines - number: PBFT: about 440 lines (6 h) plus about 2,400 lines (1 week) - number: development effort reduced 70%-97% for Multi-Paxos at over 97% of IronRSL's throughput - limits: Actions that say only that some choice exists must be implemented by hand. Operations on collections sometimes need hand-written proof hints. AutoMan gives no guarantee about proof automation. It does not cover protocol redesign. It claims that the implementation matches the spec and is safe. It proves no new theorem that a response eventually arrives. - how much was read: most of it read - source; notes: AutoMan: Facilitating Verified Distributed Systems Development Through - record id: `automan-2025` - Bolotina et al. rotor/bitme CFLOBDDs (2025) - title: Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams - what: Presents rotor, which generates BTOR2 bit-precise models of user-space 32/64-bit RISC-V integer machines, and bitme, which unrolls those models for bounded checking using Z3/Bitwuzla and byte-oriented ADD/CFLOBDD domain propagation. The paper defines rotor models as (states, initial states, transition, bad states, good constraints), k-satisfiability, and a reachability correspondence proposition, while explicitly marking formal proof of rotor correctness as future work. Bitme tracker algebra maps bounded input domains to state values; soundness/completeness are conditional on correct BDD and SMT implementations and only hold modulo timeout and bound k. Arrays are flattened to bitvectors for propagation. In 18 microbenchmarks, most samples time out under SMT or constant propagation but finish with BDD propagation; ROABVDD is faster, whereas CFLOBVDD memory scales better on increasing input complexity. The study also identifies regressions and array-unfolding limitations. - number: 18 sample programs - number: 900 s timeout - number: three runs per sample - number: RV32I/RV64I with about 100 integer instructions - limits: Rotor models only user-space RV32I/RV64I plus M, compressed instructions, selected system calls, segmented 4GB memory, and bounded input bytes; floating point, more system calls/failure modes, liveness/fairness, symbolic console arguments, concurrent code and program equivalence remain future work. The reachability proposition assumes read consumes one byte per call. Bounded checking says nothing beyond k. Domain propagation is limited to input bitvectors up to 8 bits and arrays are not natively handled; fixed input order can cause exponential BDD growth. Experiments average three runs, use an unreported 18-program supplementary suite, and impose a 900-second timeout. - how much was read: most of it read - - record id: `bolotina-et-al-rotor-bitme-cflobdds-2025` - CCF smart casual verification (2025) - title: Smart Casual Verification of the Confidential Consortium Framework (CCF) - what: Industrial experience applying TLA+ specification/model checking, weighted simulation and implementation trace validation to the existing C++ Confidential Consortium Framework. Separate node-consensus and client-history specifications are aligned with production protocol details and incorporated in CI. The paper reports six consensus bugs found/fixed and a clarified read-only consistency limitation, plus tooling/effort and state-exploration measurements. Reconstructs all six safety/liveness cases and the unsuccessful first fix, distinguishes trace compatibility from universal implementation refinement, records granularity alignment via composition/stuttering and incomplete-state reconstruction. Saves all scale/coverage rows, effort figures, counterexample sizes and issue pointers. Preserves TEE/model trust, bounded exploration and non-linearizable read-only semantics; no all-executions C++ correctness theorem is claimed. - number: Six subtle bugs found, five concerning safety and one liveness - number: 400 LoC Trace spec; 88 commits to it and 107 changes to the consensus spec; implementation 63 kLoC C++ - number: six subtle bugs found - number: 63 kLoC in C++ (§2) - limits: §§1–2: CCF runs application logic inside trusted execution environments while treating operators, host OS/hypervisor, network and storage as corruptible. This paper checks distributed protocol behavior under modeled failures, not hardware/firmware isolation, enclave security, cryptography, all 63k C++ LOC, or arbitrary Byzantine behavior of the protected consensus code. Production use in Azure Confidential Ledger is context, not evidence that every production behavior is covered. §§1.1,4,8: Smart casual verification combines formal specification, finite model checking/simulation and tests/trace checks. Consensus spec is unbounded but exhaustive checking restricts terms, requests and reconfiguration sequences. No TLAPS safety/liveness proof for all sizes or universal code-refinement proof is reported. Most CI exploration relies on bounded simulations because sufficiently realistic exhaustive exploration is too expensive. §2: CCF returns transaction results before replication; clients separately query Pending/Committed/Invalid status. A returned result may later be invalidated. Committed read-write transactions are strictly serializable; committed read-only transactions are serializable and may be stale. Pending branches offer fork-like consistency rather than arbitrary results. Broad prose about all committed transactions being linearizable needs the explicit read-only exception. §2: Transaction IDs are lexicographic term/index pairs. If two transactions commit, ID ordering agrees with execution ordering. Ancestor Commit says committed <t,i> implies same-term <t,j>, j≤i, committed. This concerns transaction identity/status, not a proof that any stale read immediately observes the newest committed write. §2.1: CCF customizes Raft with signed Merkle-root transactions, messaging without RPC correspondence, optimistic sentIndex advances, express catch-up, CheckQuorum, bootstrapping/reconfiguration and retirement/ProposeVote. A transaction is committed only after a subsequent signature is committed. The actual combined protocol needs verification; citing the base Raft proof does not establish these extensions. §2.1 reader qualification: Early description says an AE-ACK carries the last transaction in the follower log, while the Inaccurate AE-ACK bug/fix later constrains that index to the end of the received AE. The historical/protocol-description distinction must be retained rather than treating the early sentence as the final safe response rule. §§2.1,4: Reconfiguration needs majorities in each active configuration, rather than a majority of their union. A removed node remains retiring until retirement information is safely committed for future leaders. CheckQuorum steps down an isolated leader, but absent delivery/scheduling assumptions this is not a theorem that all executions make progress. §4: Consensus has 17 actions/13 variables, 12 local-state mappings plus network. Parameterization includes every nonempty initial node subset with any member as initial leader. Locally initiated timeout/signature/candidacy/step-down choices impose no clock synchrony. LogInv compares pairwise committed-log prefixes; AppendOnlyProp prevents committed-prefix rollback over time. Another 27 properties include MonoLogInv, requiring term increases only after signatures. §4: Simulation explores behaviors to bounded depth under a time quota; authors manually downweight failures to promote forward progress. Q-learning was implemented in TLC but no state-hash feature set beat manual weighting. More progress-rich traces may help find bugs but do not constitute exhaustive failure coverage or proof of liveness. §5: Client model uses append-only history and logBranches, independent of node count. History includes read-only/read-write requests/responses and status responses, but omits status requests/Pending replies. A simple shared value appends transaction identifiers so conflicts and observations are visible. It is a deliberately selected application workload, not a proved reduction of all arbitrary CCF application semantics. §5: A new branch can be any prefix of an existing branch containing the last committed transaction. Requests may execute at any still-active leader/term. PrevCommittedInv checks same-term committed ancestor statuses; ObservedRoInv demands that a subsequently committed read-only response observe a read-write transaction whose response preceded its request. The latter expectation is falsified and documented, not a proved CCF invariant. §6.1: Scenario driver serializes consensus execution deterministically and mocks governance/networking/other components, injecting loss/reordering/partition/delay. Original 13 scenarios and about 1.6k unit-test/2k Python end-to-end LOC precede the effort; Table 1 gives later exact scope counts. Initial fuzzing was abandoned for insufficient interesting coverage. Driver/mock accuracy is a boundary, as demonstrated by retirement bugs. §6.1: Driver uses a global logical ordering clock; distributed Lamport/vector alternatives are suggested but not implemented here. Fifteen added logging statements capture stable states at message and role-change points, immediately after a global lock for state changes. Constant-space values such as log lengths are recorded, not full log entries. Production logging compiles out, so the checks use instrumented test executions rather than continuous production monitoring. §6.1/§6.5: Traces initially remove/deduplicate bootstrapping events because early consensus spec omits that phase; later specification is expanded to model bootstrapping more faithfully. These describe successive coverage stages. A successful preprocessed trace validates only its retained observations and modeling assumptions, not excluded initialization behavior. §6.2: Trace spec checks existence of a spec behavior consistent with observed events/values: T∩S is nonempty. Nondeterministically reconstructed hidden state is existential. A successful finite trace check is evidence for those observations, not proof that all completions, all execution traces or unlogged state transitions meet the spec. If logging or mappings omit a decisive distinction, an incorrect implementation could remain compatible. §6.2: Send actions constrain current state, invoke high-level action and assert matching successor messages. Network changes from set to multiset to represent duplicate/resend occurrences. Trace network abstractions also explore ordering/duplication/loss guarantees. Such abstraction choices affect what is observable and accepted; they are not runtime network guarantees inferred from traces. §6.2.1 Listing 5: UpdateTerm·HandleAppendEntriesReq composes two model actions into one implementation receive. IsFault·Next admits unlogged network faults before a step; send-response events may stutter high-level variables when already modeled by another action. Composition hides intermediate states and stuttering changes observation granularity, so correctness depends on the mapping retaining semantically important events. Merely making a mismatch disappear is not an independent proof. §6.2.2–6.3: Start with a happy-path trace, add many assertions and cross-references, debug source and formulas. Invalid traces may indicate bogus logging, incorrect mapping, specification error or implementation bug; failure lacks an ordinary model-checking counterexample. Longest matching prefixes, unreachable-state graphs, failing subformulas and an unsatisfied breakpoint support diagnosis. §6.4: DFS stops after finding one compatible behavior, avoiding BFS enumeration of alternatives; a consistency trace goes from about one hour to under a second. This is an author example without trace-size distribution or controlled speedup suite, and does not mean all traces validate in under a second. Existential acceptance is essential to that optimization. §6.5: Logging/driver enhancements took about one day. Consensus alignment/tooling took two engineer-months over four months, including TLC composition/DFS/debug support, discrepancy diagnosis and abstraction design. Writing about 400 lines of Trace was minor; Table 1 counts 369. Trace saw 88 commits and consensus spec 107 changes. This is observed project effort, not a controlled productivity study. §6.5: Client consistency validation uses REST observations without source instrumentation, reconstructs other clients’ hidden transactions from observed IDs, and took about one engineer-week over two weeks, mainly by CCF experts. Smaller spec, previous experience and reused TLC changes confound a simple comparison with initial consensus effort. §7 Table 1: Approximate state counts/rates are measured on Azure DC8s v3. A log line is largely equivalent to a model action, according to authors, not a formal equality of semantic coverage. Different abstraction sizes, bounds, durations and distinct/generated-state counting prevent treating orders-of-magnitude state counts as a calibrated defect-detection probability. §7: Six serious consensus bugs comprise five safety issues and one liveness issue, found by combined modeling, source scrutiny, trace mismatch, simulation and functional/end-to-end reproduction. They are not six independent discoveries by model checking alone. Read-only non-linearizability is an additional documented consistency ambiguity and accepted behavior, not a seventh fixed consensus bug. §§7–8: Authors report all six fixed before user impact/customer reports; software had already been deployed. One-node-at-a-time operational reconfiguration masked the election bug, and absence of an incident from the first bad commit fix was attributed to chance. No external incident audit, current repository verification or independent bug reproduction was done in this reading. §§8–9: Paper chooses model checking for developer accessibility rather than deductive proof, despite compute cost. AI-assisted proof search is future possibility with a reference to neural theorem proving, not an experiment using LLM agents. Related-work sentence says IronFleet and Verdi both proved Raft; reader qualification: IronFleet uses a Paxos-based replicated state machine, so do not propagate that comparison as fact. - how much was read: most of it read - source - record id: `ccf-smart-casual-verification-2025` - Deriving Semantic Checkers from Tests to Detect Silent Failures in Production Distributed Systems (2025) - what: T2C transforms existing distributed-system tests into runtime semantic checkers. It slices assertions into parameterized functions, obtains symbolic triggering histories and constraints from instrumented test execution, mutates these histories, then filters candidates by compilation, JVM verification, self-validation and cross-validation. A production monitor matches traces and invokes checkers. The paper measures checker generation, detection after known failures are triggered, false alarms and performance; it does not prove transformation or checker soundness. Records exact extraction/precondition/mutation mechanisms, observational filtering and unsoundness, four validation levels, trace matching and distributed adapters, all study and generation counts, all twenty failure outcomes/times and issue identities, manual integration effort, false alarm denominators/counts, full cost tables, missed cases and newly added HB2 test, and a distinct newly reported ZooKeeper defect. - limits: §§2–3,8: Existing assertions encode useful intended semantics, and test-derived checks generalize beyond their original inputs/configurations. This is an explicit empirical assumption, not established for every test. The study randomly samples 35 tests per system, 210 total; subsequent percentages use only 183 assertion-bearing tests. Equal per-system sampling does not estimate the pooled distribution of all tests by test-count weight. §4.1: Backward data/control slicing preserves relevant branches, explicit aliases, local computations and assertion dependencies. It stops at operations classified as side-effecting by purity analysis plus manually supplied exclusions. No soundness guarantee; missed effects can survive. Section 4.1 says validation exposes missed operations, whereas §8 expressly denies a full guarantee of freedom from side effects. No formal refinement between a test and generated checker is established. §§4.2–4.3: Trigger preconditions are observed server-side call sequences before assertions, excluding operations performed by the checker itself. They are not Hoare-logic weakest preconditions. Analysis depends on chosen instrumentation, recorded execution, API wrappers and manual parsing/adapters. Unobserved paths and system configurations may affect applicability. Enum arguments remain concrete by default. §4.2.2: Equality of observed constants yields shared symbols; accidental equality can over-constrain and suppress checker activation. Simple less-than/contains constraints supported, arbitrary semantic relationships not inferred. Missing complex constraints or broad mutation can over-generalize and cause false alarms. Reduce/insert-wildcard/duplicate/reorder mutations are bounded enumeration; bounds, completeness and global coverage are not established. §4.4: The paper calls 672 outputs verified, meaning they passed empirical/syntactic filters: compilation, JVM sanity checks, rerunning source tests with the checker, then other passing-test workloads. Neither JVM verification nor passing tests proves semantic validity, absence of false positives, complete detection or freedom from side effects. Cross-validation assumes passing-test executions are suitable nonfailure examples; unexpected alerts could also expose real defects, a reader inference not systematically studied here. §5: Circular-buffer trace expiry bounds memory but can discard needed history; precise buffer capacity and complete-coverage guarantee are not given. Reversed precondition trie matches current trace suffix. Configuration requirements checked at startup, with no general claim of adaptation to later configuration changes. Instrumentation, runtime matcher, target methods queried, assertions, adapters, Java/Soot/Javassist and trace transport are trusted operational components. §5: Multiple clients may collectively supply a trigger sequence; cluster mode forwards traces and invokes assertions on respective nodes via RPC. No theorem establishing causal ordering, globally consistent observation, race-free semantic checking across arbitrary interleavings or distributed snapshot correctness. The runtime architecture avoids worker/evaluator buffer races according to authors; that claim is narrower than distributed checker soundness. Special concurrency properties still need carefully designed checks. §§6–7: Implementation is Java only; C/C++ port through LLVM is proposed, not evaluated. Setup includes core classes, about six unsafe operations and about three utility-adapter classes per system, beyond 42-line average configuration. HBase integration one person-week. Claims of little manual effort concern this measured support, not zero domain knowledge. §7.2: Tests selected by system-test package groups, excluding low-level data structure tests and assertion-free performance/stress tests. Target-test denominator 2172, generated functions for 2019, healthy 1933 and final 672. Final outputs cover available test semantics only. Section 4.1 describes one checker per assertion while §7.2 reports 4.3 assertions per checker; paper does not reconcile granularity, so both statements retained. §7.3: Benchmark construction starts with keyword-filtered issues, then 56 randomly inspected, 24 qualifying silent failures and 20 reproducible cases; four lack reproduction information. Reported 15/20 detection is conditional on failures already triggered, not a bug-triggering success rate or representative prevalence estimate. Reproduction takes about one week per case. Generation excludes tests reproducing benchmark failures, but baseline event checkers use historical failure examples; no universal equivalence of training information is claimed. §7.3: Missed five cases include absent semantic coverage and poor/non-generalizable assertions. HB2 only becomes detected after authors add a new test; this does not change original 15/20 result. New ZooKeeper 3.9.2 bug is a separate fault-injection finding, not an additional benchmark hit. Source calls version latest at publication; no current-version claim. §7.4: False alarm ratios use checker invocations in failure-free scenarios over 30 minutes, with Jepsen network faults every 10s. They are not alarms per hour or precision among alerts, and do not estimate arbitrary production workloads. 56% average checker activation leaves many checkers unexercised. No repetitions, confidence intervals or broad deployment duration reported. No noticeable harmful checker effects observed is empirical, not a safety theorem. §7.5: Four benchmark workloads give throughput losses 1.4/9.1/3.8/1.5%, mean 3.95% rounded 4.0. Low activation contributes to low overhead and also limits exercised semantics. No universal cost bound or worst-case under high checker activation. CPU percentages sum across cores; increases must not be read as fractions of a single total CPU. Offline build/validation take hours despite slicing taking minutes. Tables1–2: Same-version study/generation test counts differ (ZooKeeper 434 vs428, Cassandra 4118 vs3283, HDFS 3265 vs4304), without reconciliation. Table1 prints CephFS 1.11.0 and Mesos 18.2.0; preserved as printed rather than silently correcting versions. These are source discrepancies/labels, not independently checked software inventories. §8: LLM-assisted analysis, sandboxing and formal verification of generated checkers are future work. Paper evaluates no Verus, verified Rust, TLA+ or LLM-written proof system, and establishes no universal distributed-system correctness theorem. - how much was read: most of it read - source - record id: `deriving-semantic-checkers-from-2025` - Ellsberg (2025) - title: Runtime Protocol Refinement Checking for Distributed Protocol Implementations - what: It monitors the messages going into and out of a deployed process. It searches for an allowed run of a TLA+ protocol, translated to Go, that explains them. If none exists, it reports an error. It was applied to Etcd, ZooKeeper and Redis Raft. - number: executable spec sizes: ETCD 952, RedisRaft 894, Zookeeper 989 lines (prose says about 500 and 2,000) - number: mapping code 356, 370, 380 Go lines; 11, 31, 10 modified functions - number: translation tested on 8,750,468 Raft and 1,904,456 ZooKeeper traces - number: ten bugs, nine previously known, one new Redis Raft reconfiguration bug - limits: It handles fail-stop faults only. It assumes the supplied protocol is correct and the trace is faithful and ordered. It cannot prove correctness or catch livelock or deadlock. Humans wrote the translations and mappings. There is no public repository. - how much was read: most of it read - source; notes: Runtime Protocol Refinement Checking for Distributed Protocol Implemen; notes: Runtime Protocol Refinement Checking for Distributed Protocol Implemen; notes: Runtime Protocol Refinement Checking for Distributed Protocol Implemen - record id: `ellsberg-2025` - MongoDB conformance blog (2025) - title: Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs - what: This 2025 retrospective describes MongoDB engineers testing whether C++ implementations conform to TLA+ specifications. It contrasts model-generated tests with trace checking, reports practical obstacles such as mapping implementation state back to the model, and describes a Raft-derived replica-set model with safety and liveness properties. - number: The post revisits two MongoDB products and work first tried in 2020. - number: A month to figure out how to instrument MongoDB - number: 4913 tests reached 100% branch coverage - limits: Trace checking and generated tests are incomplete samples; the post says completeness is usually impossible. - how much was read: most of it read - source - record id: `mongodb-conformance-blog-2025` - OwlC (2025) - title: OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries - what: It compiles a checked Owl protocol design into executable Rust plus a Verus specification. Verus then automatically checks that the code matches the spec and avoids operations that depend on secrets. Case studies include new WireGuard and HPKE designs. - number: WireGuard: 910 Owl lines, 6,499 Verus lines, 659.8 s Owl check, 13.1 s Verus check - number: HPKE: 332 / 4,030 lines, 83.0 s / 7.8 s - number: Otway-Rees: 221 / 5,210 lines; Basic-Hash: 52 / 849 lines - number: OwlC compiles to Verus in under a second - limits: It covers secrecy and authenticity, not progress in distributed systems. The spec compiler, crypto bindings, Owl, Verus and rustc are trusted. WireGuard's UDP, device and rekey timers are out of scope. Designs do not start from vague English. - how much was read: most of it read - source; notes: OwlC: Compiling Security Protocols to Verified, Secure, High-Performan - record id: `owlc-2025` - PGo issue 259 (2025) - title: Parsing Error Defaulting to CHOOSE - what: An open PGo issue reports that a malformed TLA+ operator produces a misleading parser error saying `CHOOSE` was expected. The issue includes a minimal module and the parser's location and message. - limits: This is a parser usability bug report; it does not show a wrong verification result or a distributed implementation failure. - how much was read: most of it read - source - record id: `pgo-issue-259-2025` - ProofWright (2025) - title: ProofWright: Towards Agentic Formal Verification of CUDA - what: An agent writes VerCors annotations (permissions, preconditions, invariants) for CUDA kernels. It repairs them using verifier errors. A second path derives a proof of equivalence to the PyTorch reference, via Rocq. - number: 100 KernelBench L1 problems: 74 pass memory safety and race freedom, 17 solver instability, 9 agent failure - number: 14 simple kernels get safety plus equivalence; 3 loss functions partial - number: About 3 minutes per kernel - number: Ablation: no guide gives 0, few-shot only 13% - limits: A persistent annotation guide was seeded from 10 manual kernels, and every update was reviewed by hand. The link from Rocq to VerCors is untrusted and was checked manually. The proof agent's model and budget are not stated. There is no liveness. There is no repository link. - how much was read: most of it read - source; notes: ProofWright verifies concurrent GPU code, with a human-reviewed transl - record id: `proofwright-2025` - Remix (2025) - title: Multi-Grained Specifications for Distributed System Model Checking and Verification (Remix) - what: Refines coarse TLA+ protocol actions into detailed ones where concurrency matters. It mixes levels of detail to keep model checking practical, and checks the model against implementation executions (ZooKeeper). - number: six severe bugs violating five types of invariants - number: Six deep ZooKeeper bugs found and fixes verified - number: abstract: found six severe bugs that violate five types of invariants - number: six severe bugs - limits: The notes infer that matching the implementation and fixing bugs found by the model checker do not validate the chosen client guarantee, and do not prove liveness for unbounded cases. - how much was read: most of it read - source; notes: Choosing top-level distributed guarantees and trusted boundaries; notes: Appendix B: Concrete systems and theorem scope - record id: `remix-2025` - Sync/Async functional distributed verification (2025) - title: Functional Reasoning for Distributed Systems with Failures - what: Defines twin Rocq-embedded languages Sync and Async to make high-level functional reasoning about asynchronous distributed protocols precise, then proves that compiled Async executions are included in Sync denotations. The authors mechanize the framework and safety proofs for Bosco and Sequential Paxos. Sync is a choreography language whose typed programs are ordered communication steps over role-indexed vectors; its power-set denotation explicitly enumerates message loss, reordering, truncation and arbitrary Byzantine injections. The configuration model separates good, crash-prone and Byzantine nodes and uses a Netwk relation as an executable over-approximation. Finite loop unwinding supports safety proofs for nonterminating protocols. Bosco proofs derive a strong one-step theorem for n>7f and an inductive univalence/agreement invariant for n>3f. SeqPaxos proofs use a weakest precondition UC_D to show once a value is decided, later iterations decide it or abstain when n>2f; the condition is weaker than the protocol’s strongest postcondition and exposes optimization opportunities. Async is a monadic node LTS plus single-use channel LTS; alignment permutes arbitrary interleavings into channel order, and adequacy (Theorem 5.1) follows through aligned traces, big-step semantics and channel-erasure lemmas. The Rocq development is about 2.5k lines and includes endpoint projection/executable extraction. - number: Rocq mechanization about 2.5k LoC - number: Bosco one-step threshold n>7f; agreement threshold n>3f - number: SeqPaxos agreement threshold n>2f - number: SimpleVote example n_R=4, f_R=b_R=1 - limits: Sync excludes branches and loops inside a body, cryptographic primitives, and arbitrary communication order; it therefore targets streamlined communication-closed protocols. Network messages are authenticated, nonduplicated, eventually delivered between correct nodes, and well typed; signatures and parsing are assumed rather than modeled. Byzantine behavior is over-approximated and can inject values it could not know. Safety is proved for finite loop unwindings, not termination/liveness. The Async adequacy theorem is inclusion (compiled outputs are in the denotation), and correctness depends on the stated channel-ordering and synchrony-reduction restrictions. - how much was read: most of it read - source - record id: `sync-async-functional-distributed-verification-2025` - TraceLink (2025) - title: TraceLink: Linking Implementations with Their Verified Designs - what: TraceLink records traces from Go code that PGo compiled from an MPCal design. It converts them to TLA+. TLC then checks that the observed actions follow the design's next-state relation. It finds deviations between the implementation and the model. - number: 9 previously undetected bugs (2 network-assumption, 1 miscompilation, 2 instrumentation, 2 timeout-model, 1 failure-detector, 1 symbolic-abstraction) - number: Median tracing overhead 23% (37% with stress testing); Sidestep shortens counterexamples by 29%; 93x compression of generated TLA+ - number: 20,485-step Raft trace: 328 s vs 9.4 s plain TLC; raftkvs 990 MPCal / 7,993 TLA+ / 3,163 Go lines - number: Manual comparison for a small lock service took 2 hours (anecdote) - limits: It needs a formal design written by a human. Traces must start at the modeled initial state. It checks refinement only on the executions it observed, not on all executions, and not progress. The trace translation and TLC are trusted. - how much was read: most of it read - source; notes: TraceLinking Implementations with Their Verified Designs; notes: TraceLinking Implementations with Their Verified Designs - record id: `tracelink-2025` - VEP: A Two-stage Verification Toolchain for Full eBPF Programmability (2025) - what: VEP separates eBPF verification into C-level symbolic execution and SMT proof generation in user space, compilation that translates code, assertions and proofs, and independent bytecode symbolic execution/proof checking intended for kernel space. Separation logic describes owned memory and helper-acquired resources. Annotations expose loop invariants and contracts unavailable to fully automatic verifiers. The paper reports acceptance/rejection, time, memory and annotation/proof sizes on 41 small programs, and claims Coq proofs of the separation-logic transformation properties. It does not present a mechanized soundness/refinement theorem for the entire executable toolchain. Records proof-generation/checking boundary, trusted helper specifications and bytecode semantics, assertion restrictions and conversion rules, compilation passes and source-property loss, safety versus intended functionality and termination proof limits, concrete string/list/socket examples, all Table 2–5 results and deployment/version uncertainty. Separates sample success from universal no-error/full-programmability claims; checks discrepancies in memory/speed/acceptance prose and proof-line terminology; preserves printed illustrative inconsistencies without claiming implementation defects. - limits: §§2/5: Claimed small trusted computing base excludes the C verifier, compiler and SMT solver because bytecode is checked again. Guarantee still depends on correct executable bytecode checker, faithful eBPF instruction/memory/arithmetic semantics, actual helper contracts, and correspondence with kernel execution/JIT. The paper supplies no whole executable-checker soundness or code-to-kernel refinement theorem. §5 specifically reports Coq proofs for separation-logic transformation properties, not all these components. §§2.1/3/5: VEP-C computes strongest postconditions, eliminates spatial entailments, and uses its own SMT solver producing cvc5-style proof terms. VEP-eBPF independently symbolically executes bytecode and checks spatial/pure proof steps without solving. Checked proof terms remove the need to trust SMT answers only to the extent proof rules and their checker/semantics are correct. Kernel-space deployment is the intended architecture; evaluation does not clearly distinguish an in-kernel deployment benchmark from standalone checker measurements. §§2.2–2.3/7: Introduction and capability section claim functional correctness, but §2.3 explicitly makes user intent the user’s responsibility and §7 lists functional correctness as future work. The reported Key_connection annotations are expressly memory-safety-only. Accepting bytecode safety does not establish intended lookup/copy semantics or preservation of arbitrary source assertions. §2.2: Termination within finitely many steps is claimed. The shown loop reasoning uses invariants and exit conditions; no explicit general ranking-function, decreasing variant or fuel/step-bound rule is explained. Invariant preservation alone establishes partial correctness, not termination. This is a limit of the presented justification, not a reproduced checker counterexample. §§2.1/6.2/Appendix B: Full programmability and no false positives/negatives are author claims. Finite examples and annotations do not establish completeness for all safe programs; general entailment is acknowledged undecidable. Spatial-expression scope restrictions reject some natural quantified array assertions, requiring custom predicates. Appendix B DNF normalization can multiply branches, so approximate linear symbolic-execution cost in statement/assertion length excludes assertion-size growth and SMT solving. §3: Memory ownership uses disjoint spatial conjunction; duplicated ownership is inconsistent. Built-in helper contracts are derived from documentation, not proved against kernel helper implementations. Resource acquire/release soundness depends on their completeness and accuracy, including permitted null returns, flags and sizes. Contract variants are selected for supported contexts. §§2.3/4: Source C undefined behavior can compile into memory-safe bytecode. Early source rejection protects source semantics beyond kernel bytecode safety. Maliciously altered bytecode with a valid safety proof may pass without matching original program intent. Neither final safety checking nor an unverified compiler automatically proves C-to-bytecode functional refinement. §4: Compiler uses nanopasses, member-to-offset conversion, calling convention transformation, iterated register coalescing, and explicit stack frame preconditions. Few optimizations supported. Dead source variables become existential logical variables. Figure 14 deliberately turns a false source assertion x==1 after x=0 into satisfiable exists _x,_x==1; source assertion truth is lost even though bytecode safety can survive. §4 Figures 13/15, Appendix A: Printed illustrations contain apparent inconsistencies. Figure 13 sets R1=0 then asserts R1==*(R10-4)+1 while stack value is0. Figure 15 declares fields x,next but accesses l.head. Appendix A transforms forall n,v!=n*n into forall n,n!=n*n, which fails for n=0/1 and is not generally equivalent. These are source illustration issues; artifact behavior was not tested. Appendix A prose also describes x as a nonsquare although displayed condition constrains v with x=2*v. §3 Figures 4/6/9/12: An arbitrary owned output list proves initialized memory/ownership, not that memset filled every byte or strncpy copied/padded correctly. Figure 9 uses stronger repeat(v,n) content predicate; Figure 6’s displayed successful strncpy postcondition is weaker than complete C-library functionality. Keep actual predicate content when evaluating generated proofs. Appendix B: Internal assertions separate program-variable addresses, pure facts and owned memory; logic variables in spatial facts require permitted existential binding. Printed array-address conversion shows V(e1+e2) without explicit element-size scaling; semantics/type conventions would need inspection before inferring a compiler defect. §6: Evidence is 41 selected small C programs, not large production services or adversarial bytecode fuzzing. Linux Kernel5.15 and PREVAIL August2024 used. Hardware, trial repetitions, confidence intervals, human annotation time/user study and whole-tool LOC are not specified. No independent reproduction performed. §6 Tables 2–5: Passing rate means acceptance for safe cases and rejection for unsafe cases. All ten unsafe cases stop at VEP-C; compiler/eBPF columns are dashes. Thus data demonstrate C-front-end rejection, not independent final-checker rejection of ten crafted attacks. Safe VEP outcomes are 30 category samples plus one Key_connection, all accepted. §6.2: Linux 6/10 acceptance is for the PREVAIL sample category, not all safe programs; Linux category is9/10 and Stringlib3/10, with Key0/1. PREVAIL10/10,8/10,1/10 and Key0/1. Source attributes PREVAIL variability to SMT dependency/nondeterminism although introduction describes abstract interpretation; no experiment establishes that causal claim. Claimed version regressions30%/20% lack paired version tables, and no cross-version VEP study is shown. §6.1: Claimed predictable2–3MB VEP-eBPF memory is contradicted by Linux sample maximum8034KB (lathist); VEP-C maximum32569KB. Linux average.94ms applies to its accepted Linux sample subset, not all benchmarks, and Stringlib maximum2.69ms. Claimed3–5x faster than PREVAIL is not uniform: Linux category12.48/8.42≈1.48x, while39.46/8.42≈4.69x relative to VEP-C. Different acceptance sets complicate average comparisons. §6.3: Table3 labels proof counts as proof lines, while prose calls64840 proof obligations. Do not infer64840 independent obligations. Annotation lines are a size proxy, not measured effort or expertise. Key proof5819lines in table versus about5800 in text; preserve rounding. §7: LLM generation of annotations, broader functional correctness and advanced optimization support are proposed future work. No LLM agent experiment, Verus/verified Rust/TLA+ proof, distributed-protocol theorem or code execution reported in this reading. - how much was read: most of it read - source - record id: `vep-a-two-stage-2025` - Verified floating-point interval iteration (2025) - title: A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. - what: Formally verifies interval iteration for MDP reachability from abstract Isabelle/HOL semantics through IEEE 754 double-precision directed-rounding arithmetic to generated LLVM, then embeds the code in mcsta. The proof establishes conservative lower/upper bounds, while experiments show competitive performance. Formalizes min/max MEC reductions, finite-horizon preservation, level-graph descent and convergence in reduced MDPs. Extends Isabelle’s Refinement Framework with lower/upper bounding float relations, non-NaN/non-negative restrictions, directed FMA, mixed comparisons and min/max refinements. A Gauss-Seidel interval-iteration nres program is refined to mcsta sparse-matrix arrays and LLVM; a Hoare triple links concrete outputs to abstract reachability bounds. Integration converts mcsta 128-bit rational probabilities to rounded double bounds using unverifed glue. - number: 49 QVBS instances - number: 10^6–10^8 states - number: epsilon 10^-6; iteration cap 10^7 - number: Intel i9-11900K, 128 GB RAM - limits: Convergence theorem assumes finite reduced MDPs whose MECs are trivial or bottom and target/avoid sinks; deterministic MDPs with all probabilities one are excluded from the bound theorem. Float relation restricts values to non-negative non-NaN numbers and does not prove float lower/upper convergence to one point. LLVM theorem assumes well-formed input MDP, 64-bit size limits, valid separation-logic heaps, and correctly rounded conversions; parser/preprocessing and glue remain unverified. - how much was read: most of it read - source - record id: `verified-floating-point-interval-iteration-2025` - VeriRT (2025) - title: VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems - what: A Coq framework that proves timed behavioral refinement. It shows that C programs, compiled through CompCert to assembly, match timed abstract specs. Case studies: Cristian clock sync, a simplified PALSware, and an active/standby scheduler. - number: C lines: 313 (ClockSync), 327 (PALSware), 352 (Active-Standby) - number: ImplVerif proof lines 3526, 5913, 4718 - number: refinement proof lines 6597 and 8861 for ClockSync and PALSware - number: no person-time - limits: Timing bounds are assumptions validated outside the proof, not derived. It does not claim a per-request progress theorem. - how much was read: most of it read - source; notes: VeriRT: An End-to-End Verification Framework for Real-Time Distributed - record id: `verirt-2025` - Anvil (2024) - title: Anvil: Verifying Liveness of Cluster Management Controllers - what: Rust controllers are written as state machines. The authors prove they match an abstract model. They also prove that the model reaches the desired cluster state and then stays there, once the desired state stops changing. They call this eventual stable reconciliation. - number: ZooKeeper 1,134 executable / 8,352 model+proof lines; RabbitMQ 1,598 / 7,228; FluentBit 1,208 / 8,395 - number: total 3,940 executable, 23,975 proof/model, 2,326 trusted lines - number: parallel verification 154, 151, 96 seconds - number: about 2.5 person-months; first proof about two person-months, later ones about two person-weeks - limits: Trusts the temporal-logic embedding, the environment model, the specs of external APIs, Verus and the OS. Assumes faults eventually stop. The guarantee says nothing useful if the desired state changes forever. One bug came from an incomplete trusted spec of the ZooKeeper API. - how much was read: most of it read - source; notes: Anvil: Verifying Liveness of Cluster Management Controllers; notes: P06. Anvil: Verifying Liveness of Cluster Management Controllers - record id: `anvil-2024` - Correctly Compiling Proofs About Programs Without Proving Compilers Correct (2024) - what: PotPie compiles an embedded source program, its Hoare proof and its specification into a related target language, preserving a selected partial specification even when the program compiler changes other behavior. Gives a correct-by-construction CC workflow and a Tree workflow with an untrusted certificate generator or a less-assured boolean checker. Coq formalization proves conditional soundness; toy examples include deliberate miscompilation. Makes specification meaning preservation explicit via state correspondence and bidirectional assertion semantics, separately from target proof validity. Uses a manually translated implication database for consequence rules and structural compiler equations to transport other Hoare rules. Details source/target well-formedness, stack-purity obligations, certificate-versus-boolean trust, localized UIP axioms and partial-correctness/termination boundaries. - limits: Languages are simple related imperative calculi Imp and Stack, with natural-number arithmetic, functions and different variable models. They are embedded semantics, not C/Rust/assembly or machine-word execution. Practical lower-level logics, pointers, optimizing control-flow passes and scalability are future work. Partial correctness of a selected postcondition does not establish full behavioral equivalence, termination or any property omitted from that specification. Helper multiplication/exponentiation need separate termination proofs, and target termination is reproved rather than automatically transported. No total correctness of the approximation algorithms is established by their Hoare triples. Definition3 requires pre/postcondition meaning equivalence on source stores and target stacks related by the chosen bijective variable mapping. Compiling both assertions toFalse could yield a valid target Hoare triple without preserving intended meaning. CC requires specification soundness; Tree certificate validity alone does not supply it. Users manually translate a valid source implication database and prove corresponding target implications. These finite assertions can be preserved even if the whole compiler is incorrect. Automatic generation of these obligations via weakest preconditions is proposed but not implemented. CC needs structural equations for assignment/substitution, skip, sequence, if and while, plus source well-formedness and stack-preserving compiled expressions/functions. Thus arbitrary semantics-preserving control-flow transformations do not automatically qualify. Completeness language is conditional on the stated proof obligations and supported structure. Stack expressions in assignments and branch/loop tests must preserve the stack. Function-call effects/arity/stack shape require proofs. Source functions are mutation-free outside locals and immutable parameters, while target calls can access the whole stack. Definition1 constrains mapped variables/parameters but leaves extra stack suffix unconstrained. CC trust includes Coq kernel, mechanized semantics/Hoare definitions and two localized UIP axioms for assertion and function-environment types. It does not assume universal UIP. Opaque CC proof terms may retain dependency on source semantics. Tree certificate path constructs stk_valid_tree, whose Coq checking plus valid_tree_can_construct_hl_stk gives a target Hoare proof without UIP. OCaml certificate generation is untrusted for accepted checked certificates. Boolean fallback adds an unverified OCaml checker to the trust base and is not formal correctness evidence. Certificate generation can fail on mutually recursive functions or malformed trees. A boolean fallback for modular stack-purity checks does not repair this certificate limitation. Target specification preservation still needs its own user proof even if a certificate typechecks. Square-root example’s printed formal postcondition is a pair of cross-multiplied natural-number inequalities under preconditionTrue. Interpreting it as rational approximation additionally requires nonzero relevant denominators (b,y,epsilon denominator); these are not in the displayed precondition. The mathematical reading must not silently replace the stated encoded relation. - how much was read: most of it read - source - record id: `correctly-compiling-proofs-about-2024` - Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model (2024) - what: Proposes a concrete pointer-as-integer C memory interface with explicit allocation/access failstops and an implementation-specific allocation oracle hidden behind axioms. Demonstrates it in Coq with a toy RTL-to-tagged-Mach compiler/runtime, proving two-way behavior refinement under a matching memory-model instantiation. Public/private protection isolates compiler control data while allowing defined out-of-object effects among public data. Connects finite allocation/failstop behavior to compilation rather than treating OOM as undefined. Context labels let the oracle predict target stack offsets and heap placements without exposing private layout in interface axioms. A perturb operation models private-layout changes between public allocations. Gives executable tagged stack/allocator design, relational state/memory matching and explicit optimization losses from concrete addresses. Scope remains toy data-pointer compilation, with full C,function pointers and phase composition future work. - limits: Public/private(PvP) protection allows arbitrary accesses among public regions, but prevents ordinary source data-pointer accesses to compiler-private state such as saved return addresses,locals,parameters and heap headers. It is not object-granularity spatial/temporal safety or protection against data-only attacks. The axiomatic byte-addressed interface has finite word-representable nonoverlapping regions,positive nonnull bases,alignment and minimum-size constraints,heap-base uniqueness,stack/heap observation functions,load/store stability and free/perturb laws. New allocations need not be initialized to zero; contents are defined but unpredictable. Any integer may be used as an address. Loads/stores within allocated regions succeed. Outside them they may succeed,warp to public storage or failstop depending on instantiation; source axioms do not expose private addresses. LdStEq applies to any successful store; LdStNeq only restricts stores whose destination lies in an allocated region, permitting OOB warping side effects. Allocation may report OOM at any time under the generic axioms. Nonvacuity/behavior equivalence is established for the particular program-indexed instantiation matching compiler/runtime allocation, not every arbitrary oracle and not a source-only universal resource guarantee. Proof-of-concept memory is64-bit-word-addressed with no alignments, unlike the proposed byte-indexed interface. Source RTL has unlimited local pseudoregisters,straight-line function bodies,+/−,loads/stores,calls and fixed local arrays. Function calls may recurse; no intrafunction branches or full C parser/type system/struct/byte-layout implementation. Mach has fixed registers,abstract code pointers/separate code,tagged word memory,privileged/unprivileged accesses and direct named calls. Code-pointer corruption is excluded by this representation. General function-pointer protection is explicitly future work; abstract blanket control-flow-attack language does not prove secure arbitrary-C compilation. Theorem1 assumes source behavior under I(S) is not Stuck; a source typing judgment can rule that out. It compares termination with same result,divergence and failstop. Its stated ≈ equates failstops for any reason,so it does not by itself equate exact OOM versus OOB labels or failure timing/step counts. Compiler correctness uses forward small-step simulation and target determinism to obtain reverse refinement,with matching three-way source-call-stack/oracle-stack/MachSP and tagged separation-logic memory assertions. Proof statement is relative to Gallina semantics and model parameters; no real hardware,tagging implementation,Coq extraction or native compiler theorem is supplied. The simple compiler does no register allocation and stores every pseudoregister/parameter at a fixed stack offset. Runtime malloc/free are Gallina builtins using modeled memory instructions,not compiled actual C runtime. Their correctness proof does not establish performance or an external allocator implementation. Concrete addresses invalidate some nonalias-based optimizations and dead-allocation elimination when observable OOM is preserved. Proposed inlining/tailcall compatibility and modular oracle construction are not verified general multipass/full-C results; §7 describes preliminary/future work. No benchmark evaluation,execution overhead,tag hardware measurements or empirical importance of lost optimizations is reported. No artifact build,proof recheck or native program run by reader. C snippets motivate semantics; they are not validated examples of a completed C frontend. - how much was read: most of it read - source - record id: `defining-and-preserving-more-2024` - SCION router verification (2024) - title: Protocols to Code: Formal Verification of a Next-Generation Internet Router - what: Presents end-to-end verification of a production SCION border router: Isabelle/HOL refinement proves path authorization, valley freedom and loop freedom under a strong adversary; Gobra verifies optimized concurrent Go code for memory safety, crash/race freedom, finite processing and protocol conformance. Igloo soundly links protocol and code models. Protocol models progress from weak to Dolev–Yao adversaries and extract an I/O specification for code. Code proofs use four layers, modular function verification, outline statements for large functions and Gobra preprocessing that splits queries/removes irrelevant assumptions soundly. The effort discovered five protocol attacks and thirteen implementation issues; developers confirmed the issues, fixed most, and adopted stronger valley/loop checks. Weekly synchronization and version pinning handled moving code/protocol targets. - number: ~4,700 lines optimized concurrent Go - number: Five concrete protocol attacks; four resolved, one minor unresolved - number: 13 implementation issues confirmed; seven fixed, three pending discussion, remaining issue status as listed - number: Run 96 LOC and prepareSCMP 101 LOC motivated outline statements - limits: Global guarantees rely on refinement-model fidelity, cryptographic Dolev–Yao abstractions, trusted Isabelle/Gobra soundness and exact I/O-library alignment. The 4,700-line Go implementation required performance engineering; some large functions needed outline statements and solver preprocessing. One minor protocol attack remained under discussion; implementation verification was laborious and tool performance constrained progress. - how much was read: most of it read - - record id: `scion-router-verification-2024` - TLA+ trace validation (2024) - title: Validating Traces of Distributed Programs Against TLA+ Specifications - what: Presents an API and TLC-based constrained model-checking workflow that records selected specification-variable updates from Java executions and checks whether the partial trace can be completed to a behavior of a TLA+ specification. The framework traces only chosen variables/events, leaving omitted values existentially open for TLC to reconstruct. It handles stuttering steps and implementation transitions that combine multiple TLA+ actions, and uses shortest BFS counterexamples or constrained DFS for speed. Case studies include Two-Phase Commit, snapshot-isolation key-value store, EWD998 termination detection, two Raft implementations and Microsoft CCF; trace validation found mismatches and exposed a CCF safety bug that became regression tests. - number: Counter implementation bug detected in less than one minute with event-only trace for 16 RMs - number: Two-Phase Commit 16 RMs event-only trace explores ∞/557k states (BFS/DFS table) - number: Key-value 12-agent, 20-key/40-value event-only trace reaches ∞ states at 1-hour timeout - number: Five distributed-program case studies all yielded specification/implementation discrepancies - limits: Verdicts depend on instrumentation points, trace granularity and the high-level specification. Too-imprecise logs can admit erroneous traces because TLC fills unconstrained values; too much logging causes state explosion. TLC explores finite bounded models and can return no counterexample for an invalid trace when the searched diameter is insufficient. The method detects conformance discrepancies, not a proof that all executions of the implementation satisfy the specification. - how much was read: most of it read - source; notes: P08. Validating Traces of Distributed Programs Against TLA+ Specificat - record id: `tla-trace-validation-2024` - Trillium (2024) - title: Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - what: Trillium proves that full program executions refine a simpler model. Fairis preserves progress under fair scheduling. It uses fuel to bound stuttering (steps that change nothing). The extended Aneris shows that implementations follow TLA+ models. - number: full Coq refinement proof for the SDP example about 1,100 script lines (footnote 9) - number: cases: two-phase commit, single-decree Paxos refinement - number: Paxos client proof about 1100 lines of proof scripts (footnote 9, p.9:27) - limits: The authors translate the TLA+ models into Coq state-transition systems by hand. The distributed instantiation targets safety. Distributed liveness is future work. - how much was read: most of it read - source; notes: papers and boundaries - record id: `trillium-2024` - Verifying Software Emulation of an Unsupported Hardware Instruction (2024) - what: Coq proof that a RISC-V machine lacking hardware Mul but configured with a verified software trap handler preserves finite-execution specifications of a machine with Mul. Handler combines handwritten CSR/register assembly with compiled verified Bedrock2 decoding/multiplication. A helper ISA instance reconciles compiler assumptions with detailed CSR semantics and proves emitted code contains no Mul. Gives binary-level specification preservation quantifying arbitrary user programs/postconditions through a state relation exposing reserved-memory/CSR premises. Removes the apparent compiler/handler circularity by certifying no unsupported instructions in compiled handler code. Concrete treatment includes full register preservation including destination sp, MEPC advancement, calling convention, scratch-space bounds and CSR restoration. Evaluates a factorial program in third-party Spike, reports bugs caught by proof and external-linking bugs beyond its theorem. - limits: Case study treats M extension as containing only one Mul instruction; division/modulo/high-half multiplies are not verified here. User/handler both run in machine mode, no interrupts, uncompressed 4-byte instructions only. Abstract high-level machine has no CSR state; low-level machine has basic CSR support/configuration. Top theorem is finite runsTo specification preservation: high-level runs to post and initial R imply low-level runs to a state related to some high-level post state. It does not state equal instruction counts, cycle timing or a general reverse/infinite-trace equivalence. runsTo hypothesis carries progress/memory-safety requirements. R requires equal registers, pc, nextPc, initialized registers, basic low-level CSR fields, MTVecBase/MScratch values and separation of user-memory map from handler bytes and 256-byte scratch. User finite-map memory domain stays fixed; accesses outside it make the high-level premise unprovable. This is not protection against arbitrary user-memory corruption/adversarial writes into handler state. 256 bytes scratch includes 32 saved 32-bit register words and at least 128 bytes for compiled function stack. No assumption that user sp points to valid/free stack; handler uses independently reserved scratch. No hardware memory-protection theorem is provided; broader user/machine privilege separation is discussed as an extension. Bedrock2 compiler correctness is proved against a simpler no-CSR machine with hardware multiplication. Helper instance enforces no_mul for executable compiler-emitted handler region and transports correctness to detailed no-Mul CSR machine. This invariant is discharged from actual output, not assumed because source multiplication algorithm uses additions. Handwritten portions implement CSR behavior unavailable in Bedrock2. Compiler/program-logic proofs compose into theorem mentioning only RISC-V semantics and concrete handler bytes. Compiler correctness is proved/used internally rather than an extra trusted functional assumption, relative to Coq checker and trusted specification; no concrete CPU implementation is formally connected. Formal result applies to position-independent byte list softmul-binary. GNU toolchain ELF packaging, custom 25-line linker script, initialization and external Spike setup are unverified. A successful simulator run validates one integration instance, not the proof of an arbitrary ELF loader/boot environment. Formal Mul models 32-bit word product; algorithm uses logical shifts/addition/doubling. Scratch slot 0 may receive a computed result but architectural x0 remains fixed through machine register semantics. No separate support for compressed or all future instruction formats is claimed. Table 1 excludes dependencies (coqutil, riscv-coq, Bedrock2, compiler). Counts measure Coq source text, not assembly instruction count or human hours; generated save/restore routines expand two-line functional code to 29 instructions each. Claims of possible automation savings and a 100-line future assembly proof are conjectures. Empirical evaluation is one hardcoded factorial 5 example on Spike, not physical hardware or a benchmark suite. No repeated trials/variance, timing/cycle measurements or exhaustive invalid-instruction test corpus. Authors assess verification probably took longer than debugging; no controlled effort comparison. Reader inspected supplied paper only; no proof replay, ELF build, compiler run or Spike simulation. Related-work statements are publication-specific summaries, not independent audits of seL4/CertiKOS/CakeML. - how much was read: most of it read - source - record id: `verifying-software-emulation-of-2024` - VeriSMo (2024) - title: VeriSMo: A Verified Security Module for Confidential VMs - what: VeriSMo is a Rust security module at AMD SEV-SNP VM privilege level 0, verified with Verus. It protects its own data from an untrusted hypervisor and guest OS while providing guest page management, code integrity, runtime attestation and secret management. A machine model proves security under external interference; tracked permissions and locks verify the implementation under internal CPU concurrency. Security types constrain explicit and implicit information flow. Records exact successful-read and reachability conditions of security theorems, five preservation lemmas, initial page-table/permission assumptions, trusted hardware and byte-casting boundaries, shared-memory restrictions, register rules and declassification. Reconstructs the remapped-secret-page attack and zeroing fix, all API latency/LOC figures, baseline feature mismatch and the restricted-interrupt Linux/Hyper-V dependency. Distinguishes paper-reported proofs and fixes from independently replayed verification or exploits. - number: about 2:1 annotation/code ratio - number: about six minutes verification on 32 cores - number: 31 lines of unsafe Rust for hardware primitives - limits: §§2.1,3.1–3.2: Trusts CPU/firmware security behavior while hypervisor and guest OS may be malicious. Physical attacks are excluded and denial of service remains possible: the hypervisor can stop the host or refuse vCPU scheduling. This is a conditional safety result, not availability, scheduling fairness or distributed liveness. §§2.1,3.2: VeriSMo runs at VMPL0; guest at VMPL3, though VMPL1/2 could be used. Both use restricted interrupts, so the hypervisor can inject only #HV and a doorbell supplies the requested event. Mainstream Linux v6.8 lacked this support in KVM/guest, so experiments use Hyper-V and a modified Linux guest. The proof does not establish safety for an arbitrary unmodified VM/interrupt configuration. §§2.1,5.1: Hardware model includes CPU registers, memory, guest and nested mappings, RMP and cache/TLB-related state. E0 is VeriSMo, E3 guest, Ehv hypervisor. Guest and VeriSMo share an encryption key; VMPL access permissions separate them. Sibling VMs are omitted because the model grants the hypervisor a superset of their capabilities. Reads of externally shared memory/registers are unconstrained. §§4.2,5.1.2: External interference is handled in a machine state transition model; internal concurrency uses ownership and permissions. Primitive instruction wrappers contain trusted unsafe assembly and fully trusted postconditions derived from AMD manuals. Only critical memory/cache operations are modeled, under stated restrictions. Direct GHCB communication replaces code that might trigger #VC; unexpected #VC or other interrupts terminate the VM. Hardware-model completeness and faithfulness remain assumptions. §5.2 Listings 4–7: Confidentiality assumes an invariant-valid state, a successful secret E0 read, equal system physical addresses and a successful other-entity read; it concludes that the latter is encrypted. Integrity assumes invariant validity, attack reachability and successful E0 reads in both states; it concludes equal returned data. Neither theorem forces a read to succeed. Invariant preservation restricts E0 operations by software preconditions; attack-model closure covers arbitrary non-E0 operations. These are model-level security statements, not a complete cryptographic or microarchitectural side-channel theorem. §5.3 Lemma 1: After a validated VM-private GPA binds to an SPA, hypervisor changes leave it bound to the same SPA or make access fail, provided E0 does not revalidate an already bound GPA. Lemma 2: VM-private secrets remain encrypted to hypervisor reads; the guest C bit is required, whereas a permanently set RMP validation bit is unnecessary and cannot be assumed. A hypervisor can invalidate memory without gaining plaintext access. §5.3 Lemma 3: VMPL0-private memory remains unreadable by E3 and its E0 read either returns the original value or fails under Ehv/E3 actions. rmpadjust must not grant guest access to private pages. Lemma 4 extends same-or-fail translation from GPA to GVA using protected page tables. Lemma 5 requires a one-to-one mapping and separate page-table versus ordinary write APIs. §§5.3.3,6.1.1: Initial E0 page tables are trusted to reside in designated private PT memory and map GVAs one-to-one to GPAs. pt_write must preserve both conditions. Initial uniqueness of memory permissions is also assumed, then ownership/non-copyability preserves uniqueness. These initialization assumptions must be checked in a deployment; preservation alone does not establish the initial state. §§5.3.4,6.1: The connecting proof turns software-tracked constraints into hardware constraints when an operation succeeds. SnpPointsTo records GVA identity, optional value and software/hardware RMP/page-table/is_pt attributes. Tracked resources cannot be copied or freely constructed. Fine-grained permissions avoid carrying a global machine state through each implementation proof. §6.1.1: Object sizes, object/byte casts with consistent size and unique bindings, and raw-memory splitting/merging with consistent attributes are trusted specifications or axioms. Rust ownership does not verify these representation facts automatically. Listings 8–11 illustrate permission interfaces and deliberate rejected operations; their abbreviated syntax is not a separately compiled proof artifact. §6.1.2–6.1.3: Lock acquisition transfers a stored memory permission to the holder; release requires restoration of its invariant and returns ownership. Values can change between separate acquisitions. A local lock cannot prevent malicious guest/hypervisor access to a shared page: its permission allows copying and writing but no borrowed reference. Unrestricted reference access requires copying to private memory or safely making the page private. §6.1.4: Registers have per-CPU permissions. GHCB MSR is shared and reads are unconstrained. Writing IDTR/GDTR transfers ownership of the pointed-to memory to hardware. Explicit RIP/SP access is excluded. Updating CR3 requires mutable permissions for the page table and all usable virtual memory, so the single kernel page table is installed only once at boot. These restrictions limit the verified implementation, rather than verifying arbitrary register-manipulating code. §6.2: Security types pair a value with per-entity possible-value sets; full set means secret and singleton means public. Operators propagate sets; comparisons require public operands, and memory addresses must be public. Non-confidential memory may contain only values public to the relevant entity. Trusted downgrade converts a set to a singleton; downgraded keys fail crypto preconditions requiring full secrecy. §6.2 reader qualification: A possible-value set is not a probability distribution or an entropy bound. The paper describes a tracking discipline and trusted cryptographic interfaces, not a general proof that arbitrary full-support values are uniformly random. Binary-operator equation is printed with a op b inside a set quantified over v/u; it is illustrative notation and is not a checked artifact definition in this reading. No flaw in the external implementation is inferred. §§3.4,6.2,7.1: Only three secret categories are used: hardware VM communication keys, VeriSMo key pair and guest symmetric keys. Their uses go through a completely trusted external verified crypto library. Trust also includes ground-truth axioms, functional/security specifications, primitive APIs, Rust core interfaces, Verus and Rust compiler. External HACL verification is not re-established by this paper. §3.4: Guest page sharing must use the module API; otherwise those pages will not be validated again. LockKernel is callable once and removes guest write permission from declared kernel-code pages and supervisor-execution permission from other pages. The caller chooses code ranges; this does not establish that the chosen code is benign or that a malicious guest supplies a truthful semantic runtime measurement. §3.4: ExtendPCR maintains a hash chain beginning with starting code/configuration; Attest binds a nonce, a hardware-attested module identity and module-attested chain. DeriveKey ties a retained encryption key to the runtime measurement and guest uses Encrypt/Decrypt without receiving it. Protocol/crypto behavior and meaning of measured guest inputs depend on trusted specifications; no remote distributed attestation workflow is evaluated. §7.2: OSMEM executable ranges and tracked permission map share an invariant equating range membership with possession of page permissions. One lock protects both the bookkeeping and permission-controlled RMP modifications. Handler range checks are forced by the need to obtain a tracked page permission. This establishes specific safety/range constraints, not every possible API intent property without a specification. §8.1: API averages/standard deviations come from 100 calls each. Switch measures the full VMPL3→hypervisor→VMPL0→hypervisor→VMPL3 round trip. Attestation has much greater variability than cheap calls; LockKernel is expensive but once per session. Table 1 provides milliseconds and thousands of cycles, not proof runtime. §8.2: UnixBench compares VeriSMo, Linux-sm, C-sm and Linux. Authors report almost zero overhead and comparable performance, but do not publish per-bar confidence intervals or an all-workload equivalence bound. Figure 5 contains visible differences, including Linux above modules on some bars. Linux-sm/C-sm implement only WakeUpAP, SetPageShared and SetPagePrivate, whereas VeriSMo provides more APIs. These comparisons are not a controlled isolation of verification cost for identical feature sets. §§8.2,8.4: Up to 40% Hecate slowdown is attributed to prior work and its #VC trapping, not a new head-to-head run. AMD SVSM/COCONUT performance is not compared because the hypervisor differs. Unsafe block counts (32 VeriSMo, 150 AMD SVSM, 235 COCONUT) are source snapshots reported in 2024; lower block count alone proves neither comparative security nor absence of bugs. §8.3: Reports about six minutes for both proof layers using multithreaded Verus and Z3 4.11.2 on 32 cores. Table 2 includes 803 Verus-library axiom LOC and 101 trusted LOC as well as project axioms/trusted wrappers; the 31 unsafe Rust LOC for hardware instructions is not the total trusted code. The allocator interface is trusted, although its implementation is verified. Proof/spec annotations are approximately twice executable implementation size, not a uniform ratio for every module. §8.4.1: The remapping vulnerability was detected during verification; authors report an AMD disclosure in early May 2023 and security fix, with early COCONUT still retaining the older bug. The reading checks the paper account and cited commit pointer only, not a reproduced exploit, current project state, or independent fix audit. No artifact or proof replay was executed. - how much was read: most of it read - source; notes: VeriSMo: A Verified Security Module for Confidential VMs - record id: `verismo-2024` - Verus SOSP 2024 (2024) - title: Verus: A Practical Foundation for Systems Verification - what: A Rust verifier for systems code. In its EPR-enabled method (EPR is a restricted logic that the solver can decide), the developer writes the inductive invariant (a fact that holds initially and is preserved by every step) and the tool checks it automatically. The evaluation (Section 6, Figure 9) is at the component level. - number: 6.1K lines of implementation and 31K lines of proof - number: IronKV 1,533 exec / 4,509 proof / 1,613 trusted lines; verifies in 18 s on eight cores vs Dafny 201 s - number: node replication verifies in 9 s vs 228 s - limits: It applies to the paper's EPR-enabled method, not to finding arbitrary invariants. - how much was read: most of it read - source; notes: S30; notes: Verus: A Practical Foundation for Systems Verification - record id: `verus-sosp-2024-2024` - A Proof-Producing Compiler for Blockchain Applications (2023) - what: Augments Cairo0 compiler with per-compilation Lean3 specifications and correctness proofs connecting actual compiled Cairo machine code to user-written high-level functional specifications. Tool harvests compiler metadata and logs; it generates naive function/block specifications and proof scripts, while users prove these imply their desired specifications. Lean checks generated and handwritten proofs. Case verifies secp256k1 arithmetic and public-key recovery for signatures, conditional on model/range assumptions and an admitted elliptic-curve associativity lemma. Does not verify compiler universally or prove total correctness/cryptographic unforgeability. Cairo memory/register values are finite-field elements, memory is immutable,failed assertions have no successor and ill-formed instructions are nondeterministic. ensures quantifies over finite halting traces and promises some reached state satisfying a step-indexed postcondition; recursion/loops use induction on execution length,not a termination proof. Generated specifications use users’ specs of dependencies,allowing modular recursive proofs. Verification symbolically steps assembly via proved small-step instruction lemmas. Compiler flow-tracker identities about allocation-pointer changes are themselves proved in Lean. Range-check pointer intervals are threaded through calls; length mu<=kappa,with public execution length below field characteristic,prevents wraparound. User-facing specs mediate integers,secp field and three-limb Cairo-field representations. Only regular CFGs are supported; tool can fail on arbitrary spaghetti jumps. Generated source-level proofs support interactive debugging and incremental specification reuse without trusting compiler transformations. - number: {'math_Cairo_lines_approx': 450, 'math_Lean_spec_proof_lines_approx': 1150, 'secp_Cairo_lines_approx': 800, 'secp_spec_Lean_lines_approx': 3200, 'elliptic_group_lines_approx': 150, 'dependency_functions': 24, 'assembly_field_elements_approx': 900, 'generated_Lean_proof_lines_approx': 7500, 'admitted_sorry': 1} - limits: Cairo0 version0.10; Cairo1 substantially differs and is not the target language verified here. No separate formal source-language semantics/universal compiler correctness theorem. Partial correctness conditional on successful halting execution. STARK certification supplies evidence of such execution under cryptographic assumptions; this work does not establish termination or full cryptographic protocol security. Expected machine code/dependencies must occupy specified memory,arguments/registers must be placed correctly,range-checked region assumptions must hold and execution length must be below Cairo-field characteristic. Elliptic-curve group associativity is admitted using one Lean sorry. Paper notes a recent external formalization could eliminate it but does not claim integration already happened. Small trusted Lean kernel checks proof terms but mathematical/model assumptions remain. Repository link/archive is supplied; no independent artifact execution,trust-chain audit or kernel recheck performed for this reading. - how much was read: most of it read - source - record id: `a-proof-producing-compiler-2023` - Grove (2023) - title: Grove: a Separation-Logic Library for Verifying Distributed Systems - what: Grove is a separation-logic library for verifying distributed systems, implemented as an extension living in the Perennial repository; its README points to a VRSM case study and Go source. - number: 12x lines of proof as lines of code (§6) - number: 67-73% of single-core Redis throughput; about 2x throughput from one to three servers - number: 1,597 lines of added Coq reasoning principles - number: proof-to-code ratio around 12 - limits: README points to an SOSP paper for details; this record covers repository documentation only. - how much was read: most of it read - source; notes: papers and boundaries - record id: `grove-2023` - Hydra (2023) - title: Hydra: Effective Runtime Network Verification - what: It compiles monitor programs that operators write in Indus into P4 code. The P4 code checks each packet at every switch hop and at the last hop. - number: 11 properties in 14-64 Indus lines generating 102-211 P4 lines - number: Aether baseline 44.53% of header-vector capacity, one checker raises it to 52.14% (7.61 percentage points) - number: compiler about 2,500 OCaml lines - number: known Aether bug reproduced and confirmed - limits: The expressiveness theorem is about the language, not the network. There is no liveness. Humans write the monitors, the field mappings and the linking. The testbed could not saturate switch throughput. - how much was read: most of it read - source; notes: Hydra: Effective Runtime Network Verification; notes: Hydra: Effective Runtime Network Verification - record id: `hydra-2023` - Lightning Network TLA+ (2023) - title: Towards a Formal Verification of the Lightning Network with TLA+ - what: The paper splits the Lightning BOLT protocol into ten TLA+ specifications and nine refinement steps. The goal is to show that an adversary cannot steal an honest user's funds. Two hard steps are model checked. The rest are done by hand. - number: ten specifications, nine proof steps - number: two steps checked: (IV)=>(V) and (IX)=>(X) - number: no state counts, runtimes, LOC or hours - number: No runtime or state-count table reported - limits: It is work in progress and not a complete theorem. It does not verify code. It has no full liveness proof. - how much was read: most of it read - source; notes: Towards a Formal Verification of the Lightning Network with TLA+ - record id: `lightning-network-tla-2023` - Spoq: Scaling Machine-Checkable Systems Verification in Coq (2023) - what: Spoq translates Clang-generated LLVM IR and Armv8 assembly into structured Coq programs, then automates layered specifications and refinement proofs using CCALs. Low-level functional specifications aggregate instruction semantics; high-level specifications unfold/simplify lower interfaces into self-contained transitions. Coq checks generated proofs including Z3-suggested transformations. Evaluates translation coverage on five codebases and verifies updated SeKVM trusted core, followed by a separately written confidentiality/integrity refinement to an ideal machine. Records every CFG rewrite and specification transformation, loop ranking/branch/manual-data-abstraction limits, SC/Arm-memory bridge, security declassification model and full trust chain. Saves translation numerators/denominators, all manual-effort table cells, generated sizes and application/platform details. Distinguishes generated behavioral equivalence from desired correctness, translating Linux from verifying Linux, and changed-version/security-method comparison from a controlled labor experiment. - limits: §§1–2,8: LLVM-to-Coq translator/CFG restructuring is unverified and trusted. TCB explicitly includes Clang/LLVM toolchains, translator, LLVM/assembly semantic definitions and ultimately proof checker/model adequacy. Earlier wording only part unverified needs trust is restricted to Spoq internals, not whole stack. Coq checking does not establish the correctness of trusted translation, compilation, runtime/hardware semantics or intended property. §§2,7.2: Automatically generated specifications intentionally preserve code behavior, including bugs; behavioral refinement alone does not prove desired functionality. User must prove an independent high-level property, or supply an independently justified top-level specification. The SeKVM security proof trusts approximately200LOC ideal machine/declassification policy, not the much larger generated real-system specification as an axiom. §§4,8: Broad full-C claims mean using Clang to accept unmodified GNU-C constructs rather than verifying all C semantics/programs. Prototype supports only a subset of LLVM IR and Arm assembly; advanced callbr/invoke/resume unsupported. Only Armv8 assembly currently parsed; automatic assembly specification/proof synthesis handles no-jump procedures. All translated functions in broad-codebase experiment are representation successes, not correctness proofs. §§2–3: User supplies layer configuration, bottom machine model completion, ranking function per loop, and manual data abstractions/refinements. A layer calls only lower layers, so A→B→C requires three layers. Generated global memory/getters/setters omit concurrency event/oracle structures; these must be added manually. Cyclic function dependencies/general recursion support is not demonstrated. §4: CPU-local concurrency partitions memory into CPU-private, lock-protected and lock-free objects. Lock access requires local CPU ownership; lock-free access emits global events with environmental oracle steps. Model assumes sequential consistency. Propagation to Arm relaxed memory additionally requires six weak-data-race-free conditions as in VRM; SeKVM authors report doing this but omit details. No blanket proof for arbitrary relaxed-memory C programs follows. §§3,5: Loop ranking must be nonnegative/decrease, supplied by user and checked with xlia/induction. Fixed-point recursion has fuel and break/return flags; after flags set it preserves state through remaining recursive steps. Rank0 must not silently truncate a live loop. Loops within conditional branches need manual copied/adjusted induction templates in current implementation. No generic automatic termination/invariant discovery theorem. §5: Assembly-C linking follows AAPCS64; caller-saved registers become UNKNOWN after calls and cannot be read before write. Inline assembly may use declared C input/output operands, system registers/constants; direct general-purpose-register access disallowed. These restrictions constrain supported code despite broad inline-assembly headline. Assembly branches require user-written specification/proof. §§3,6: Automatic lifting applies to identity/no-data-abstraction layers. Mapping arrays/page tables/locks/ownership to abstract maps requires user relations, operations and proofs. Self-contained means no calls to other layers except bottom machine model, not an independently meaningful security specification or absence of all low-level detail. §6: Z3 proposes branch/rely/math simplifications; annotations guide Coq hrefine reconstruction and are removed by a final refinement. Z3/spec/proof generators are outside soundness TCB when all required proofs check. Coq tactic failure still requires manual completion. Half-second Z3 timeout reduces simplification opportunities rather than permitting unproved solver facts; large functions can take>30min. §7.1 Figure8: C translation experiment uses default source build configurations; Linux v5.15 specifically allnoconfig. Makefiles may be changed to emit LLVM .ll and ClightGen unsupported flags filtered. Reported functions are those in tested builds, not every possible kernel configuration/source path. Broad translation does not verify Linux/OpenSSL/Redis/Memcached/mbedtls properties or assembly compatibility of every function. §7.2: Verified SeKVM is already retrofitted KVM/Arm trusted core, not the entire unmodified vanilla Linux/KVM codebase. Updated RaspberryPi4 support is a modest code change with same34layers. Spoq avoids additional parser-driven source alterations to that core; verified3.8KLOC C/assembly matches compiled source, conditional on trusted compiler/toolchain. Source proof is not an independently verified binary compiler chain. §7.2 Table1: Proof cost is manually written Coq LOC, not elapsed developer time, person-months or a randomized same-version comparison. Baseline is previous SeKVM version, machine model differs, security proof changes from noninterference/data-oracles to ideal/real. Security LOC38% reduction explicitly unrelated to Spoq; functional79% reduction and total74% should not be causally conflated. §7.2: Trusted-core all3.8KLOC translation and checked proof claims are authors’ results, not replayed here. One security use case and five translation codebases do not show general automatic proof of arbitrary concurrent systems. Article gives proof strategies/examples, not complete machine-checked metatheorems of translator soundness or every reconstruction algorithm. §7.2 Table1: Original functional categories add33.5K and security38.3K. Spoq rounded component cells plus26rankinglines add≈7.026K/10.026K versus printed7.0K/10.0K; compatible with rounding. Summary ratios1/3specLOC and1.4proofLOC use approximate categories, not exact timed effort. Preserve printed percentages and units. §7.2 Figure 10: Benchmarks compare source-verified SeKVM, vanilla KVM and native on Raspberry Pi 4B, with resources matched to two CPUs and 4GB RAM. SeKVM guest uses a modified virtio driver; the other guest uses vanilla Linux 5.4; host is 5.4.55. Guest changes and one platform constrain comparison. Bars normalize native to one; lower is better. The below-15% overhead claim uses vanilla KVM as baseline. §§7.2,8: No benchmark run counts/confidence intervals/random variation are reported. Code-generation runtime2h on8core2.3GHzXeonE5-2686v4/32GB differs from execution benchmark platform; Coq-check time is not separately isolated. Timing/labor adjectives are author assessment. No concrete newly discovered vulnerability list or proof failure corpus is supplied. §9: Related-work broad impossibility/completeness claims are authors’ comparisons, not independent findings about all versions of those frameworks. No distributed-consensus theorem, Verus/Rust proof, TLA+ model or LLM experiment. Paper demonstrates proof-producing automation relevant to agents, not evaluation of model-generated specifications/proofs. - how much was read: most of it read - source - record id: `spoq-scaling-machine-checkable-2023` - Tamarin to Gobra/VeriFast (2023) - title: Sound Verification of Security Protocols: From Design to Interoperable Implementations - what: Translates a Tamarin protocol model into separation-logic specs. Gobra (for Go) and VeriFast (for Java) check these against annotated code. This carries the secrecy and authentication already proved for the model over to the implementation. It was applied to an adapted WireGuard. - number: WireGuard: 608 Go lines, 3,936 spec/proof lines, 32% generated; about 250 Tamarin rule lines; checking 148/138 s - number: signed DH Go: 106 / 1,015 lines, 61% generated; Java: 113 / 1,022, 76% - number: model verification about 3 minutes - limits: Safety only, with no progress property. The adversary is Dolev-Yao (it controls the network). Network and crypto calls are trusted stubs. DDoS handling, metrics and load balancing were removed. Observational equivalence is future work. - how much was read: most of it read - source; notes: Related work absent from the first pass: Tamarin models to verified Go - record id: `tamarin-to-gobra-verifast-2023` - TLA+ ZooKeeper reliability (2023) - title: Leveraging TLA+ Specifications to Improve the Reliability of the ZooKeeper Coordination Service - what: Builds three linked TLA+ specifications for ZooKeeper/Zab: an abstract protocol specification, a detailed system specification serving as a super-document, and a test specification that drives explorative implementation testing. The protocol model captures Zab ordering and recovery; the system model refines implementation details and uses interaction-preserving abstraction to make TLC checking feasible; the test model and Met conformance framework generate traces for the Java implementation. The authors reproduce deep ZooKeeper bugs ZK-2845 and ZK-3911 involving accepted-log inconsistency or committed-log loss, and merged the specifications into Apache ZooKeeper. - number: protocol configurations reach tens of thousands of states in seconds - number: system configurations reach billions of states and some exceed 24 hours under stated limits - number: two deep bugs reproduced: ZK-2845 and ZK-3911 - number: trace length limit 100 in simulation; model-checking time limit 24 hours and disk limit 100 GB - limits: The objective is usable specifications and automated testing rather than full verification. TLC explores bounded configurations, trace lengths and resource limits; the system-level state space can become intractable. Conformance depends on the abstraction and instrumentation mapping between model actions and implementation events, and does not prove all Java code behavior. - how much was read: most of it read - source; notes: ## ZooKeeper TLA+ specifications (2023) - record id: `tla-zookeeper-reliability-2023` - Verifiable P4 (2023) - title: Foundational Verification of Stateful P4 Packet Processing - what: Builds Verifiable P4, a Coq program logic and semi-interactive verifier sound against formal P416 operational semantics, plus a proved-correct reference interpreter. Demonstrates source-level functional correctness of a sliding-window Bloom filter and a firewall no-recent-false-negatives policy, and adapts the proof to sliding-window count-min-sketch. Section 2 connects P4 control-block proofs to functional models, abstract time-window axioms, a per-packet process relation and its flow-level history closure. Hierarchical representation predicates and MOD clauses track only the rooted persistent-register subtree, enabling client/library proofs. Sections 3–4 define P4light, big-step stack/external-state semantics, nondeterministic partially initialized bits, a determinizing interpreter and a separate static instantiation phase with fully qualified paths and abstract methods. Theorem 1 proves SBF model axioms; Theorem 2 proves the P4 control implements the model; Theorem 3 proves program-logic soundness. Table 1 records P4-manual/compiler ambiguities and fixes. Sections 5–7 report proof sizes, saturating CMS adaptation and explicit boundaries for parsing, compilation, concurrency and probabilistic false positives. - number: T=60s; k=4 panes; r=3 rows; S=2^18 slots - number: dense-flow maximum gap about 100 microseconds - number: 48-bit nanosecond timestamps with wraparound - number: SBF: 416 P4 / 480 model / 1258 specs / 1859 P4 proofs / 1261 high-level proofs lines - limits: The SBF’s no-false-negative flow theorem assumes dense monotone packet time with no gap over T/C (about 100 microseconds), enabling incremental clearing; correct switch timestamps are assumed, while 48-bit nanosecond wraparound is allowed by the proof. Parameters are T=60 seconds, k=4 panes, r=3 rows, S=2^18 slots per row. Packet handling is atomic for a single Tofino-like pipeline; multiple pipelines, recirculation and surrounding packet scheduling remain future work. The logic excludes packet parsing/deparsing although the operational semantics includes them. The P4 front end/type checker and deployed compiler are not proved correct here; architecture resource acceptance and compiler correctness are assumptions for executable behavior. The reference interpreter selects zero for undefined bits, proving one allowed behavior rather than exhaustively exploring nondeterminism. No small false-positive probability is proved. P4 type-soundness proof and broader interpreter test-suite validation are ongoing. - how much was read: most of it read - source - record id: `verifiable-p4-2023` - Automated Verification of Network Function Binaries (2022) - what: Klint checks x86_64 network-function binaries against Python specifications by symbolic execution with trusted environment/data-structure contracts. Ghost maps express both specifications and contracts, separating known key/value/presence triples from unknown-item invariants and translating operations into quantifier-free bitvector constraints. Candidate invariants are inferred across maps and weakened to a packet-loop fixed point. Optional full-stack verification follows NIC register actions and separately proved data structures/allocator. Records operation formulas, persistence layers and recursive lookup shortcut, forall incompleteness/nontermination, invariant relaxation and cross-map candidates, dynamic-link/memory/event restrictions, NIC action preconditions, precise full-stack trust boundary, all verification/performance tables and BPF scope, concrete configuration/standard bugs, appendix property obligations and get algorithm. - limits: §§1–2: Core technique assumes correctly implemented, delineated data structures with map-based contracts. Binary must expose calls/symbols for environment operations and known parameter types/calling convention. No source/debug symbols needed for NF, but this is not arbitrary opaque whole-binary verification without contracts. §2.1: Single-threaded, initialization then packet processing; no shared-state multi-thread verification. Code executes only on init/packet arrival; timers must be checked within handler. Capability allocation only at initialization and may fail externally, e.g.OOM. Later operations may fail through misuse, not arbitrary external environment failure. §5: Mutable memory after init confined to stack and map-modeled heap; other memory read-only. calloc-like allocations return symbolic pointers. State/data-structure separation is enforced, and excessive unabstracted paths reach configurable instruction threshold. No general unbounded-loop termination proof. §§3.2–3.4: Decidability concerns generated quantifier-free bitvector formulas, not completeness or termination of all host-level map/invariant processing. forall false gives no constraints on future unknown items. Recursion shortcut handles reciprocal maps but other recursive invariants may recurse infinitely; introduction always-proof-or-counterexample claim is explicitly qualified by §3.4 and execution limits. Failed checking can be incompleteness/threshold/timeout rather than an actual implementation bug. §3.4: Unknown-item invariant applies only to unknown keys, not every known item; equality consistency handles aliases and KnownSize constrains distinct present known keys. Map layers share base unknown state and lazily transform known entries so later reads on old/new versions remain related. Ordered queues/stacks are expressible but authors believe poorly suited to inference. §4: Candidate constraints from initialized/known items are relaxed until inductive over each packet path; cross-map FK,FV,FP functions are discovered from known items and checked against unknown invariants. Shrinking candidate set is paper convergence argument; this does not establish inference of every useful invariant or remove §3.4 recursive-operation nontermination. §5: Specification map matching tries candidates heuristically and rejects only after all possibilities violate spec. §6.1 requires struct field order in spec to match implementation; values can be abstracted with ellipsis. Specifications/environment contracts remain human adequacy obligations. §5: Full stack verifies driver/most minimal OS against manually encoded NIC DSL/actions from public hardware documentation. Register writes must match feasible action and preconditions; hardware semantics and model faithfulness remain trusted. Does not prove physical NIC correctness or distributed network behavior. §5: Full-stack TCB explicitly includes Klint,angr,Z3,bootloader,hardware,VeriFast and C compiler for source-verified data structures/allocator. Ordinary core-contract mode assumes those implementations correct. Abstract assertion of no trusted software except Klint omits this detailed boundary. §§5,7: Environment compiled separately, linked without LTO to retain symbols; dynamically linked data-structure operations cost calls/lost inlining. NF+driver can compile together. Containers use Linux environment/contracts and trust container runtime/Linux implementation, enlarging TCB. §§6.3,7: Seven functionally checked binaries are six C functions plus one Rust policer; five existing BPF programs receive memory safety/crash freedom only because functional specifications unavailable. Native assembly dumped from kernel-compiled BPF is analyzed with BPF-map contracts. Rust example validates one compiled binary relative to contracts/spec, not Rust language/compiler correctness or a Verus proof. §7: Correct implementation of specification is not proof of protocol properties such as absence of infinite network-message loops. No distributed consensus/liveness/linearizability/durability theorem, no TLA+ or LLM-generated specification/proof evaluation. §6.1: Verification timing from one specified CPU; solver heuristics can change times by dozens of seconds, no repetitions/confidence intervals stated. Table1 excludes additional~15minutes/fullstack/function. Router0s cells are printed values, not measured zero computational work. §6.2/Table2/Figure5: All10Gbps Klint throughput cells are link-saturated censored measurements, not true maximum capacities. TinyNF replaces original Vigor DPDK subset in principal comparison. Implementations/allocator/driver/inline assembly differ and Klint bridge adds STP; performance is not controlled same-code cost of verification. Curves show median and5th/95th percentiles, not statistical confidence intervals. §6.3/Table3: No extra inputs comparison excludes shared prerequisites: NF specification plus data-structure/environment contracts still required. Historical Rust bug-tracker69unsoundissues and BPF loop restrictions are source-time claims, not current facts. External repository/proofs unrun. - how much was read: most of it read - source - record id: `automated-verification-of-network-2022` - Cordis mCRL2 Verification (2022) - title: Formal verification of an industrial UML-like model using mCRL2 (extended version) - what: Defines Cordis low-code UML-like model semantics and an automatic translation to mCRL2, then verifies requirements of an industrial cylinder control model with model checking. The case study formalizes control requirements, exposes a false property through a lasso counterexample, and checks twelve properties in total. The discussion reports semantic discrepancies found between generated PLC code and mCRL2 translation and describes fixes and plans for symbolic/compositional checking. - number: 2 properties from §4.2 plus 10 additional requirements - number: each property verified in under 5 seconds - number: 1 false property and all other requirements satisfied - number: Cordis Modeler 3.14.1630.7156 and mCRL2 202106.0 - limits: The cylinder model is relatively simple and verification is a proof of concept. Results depend on Cordis Modeler/mCRL2 semantics and currently focus on single/limited models; complete industrial systems with interacting objects and larger state spaces require future symbolic or compositional techniques. - how much was read: most of it read - - record id: `cordis-mcrl2-verification-2022` - DaisyNFS (2022) - title: Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning - what: DaisyNFS is a Go NFS server with sequential Dafny-verified file-system methods on the Coq/Perennial-verified GoTxn transaction system. A simulation-transfer theorem converts sequential operation refinement plus safe transaction use into concurrent crash-safe trace refinement. GoTxn extends GoJournal with two-phase locking and an allocator; each visible NFS operation runs in one transaction; space reclamation uses separate transactions that are logical no-ops. Evaluation measures throughput/scaling, proof sizes, development changes and trusted-code/specification bugs found by testing. Reconstructs the four theorem/lemma roles, trusted Dafny/Coq correspondence and safe-use check, local two-phase-locking footprint invariant, nondeterministic allocator validation, rename retries and zero/free checks. Saves full API scope, proof/LOC, eleven bug and four change-effort entries, benchmark baselines and visual estimates. Distinguishes modeled network-trace correctness from wire code/spec intent, crash safety from liveness, and final LOC ratios from controlled productivity evidence. - number: only 2x as many lines of proof as code - number: unverified NFS wrapper is 1,144 lines (Figure 12, PDF p.12) - limits: §§3–4.2: The top-level theorem is network-request/response trace inclusion for a modeled server loop, not verification of every byte in the daisy-nfsd binary. Unverified Go dispatch must parse/decode correctly, call the correct method and encode results; GetRequest/SendReply are abstract I/O events. Each request executes in its own goroutine. Dafny-generated Go methods link with directly written GoTxn verified through Goose/Perennial in Coq. §§4.2,9.3: Disk reads/writes of 4KB blocks are assumed atomic; written data must persist without corruption. Initial implementation/spec disks are all zero and same size; initialize on an empty disk and run recovery after every boot. Crashes may recur and erase memory. This theorem does not cover malicious disk corruption or executions violating the assumed language/disk model. §4.1: Formal NFS state is inode→regular-byte-file/directory map plus attributes; directory names are bytes and clients resolve paths. The model is links, not an enforced directory tree. Out-of-space failures and any chosen current timestamp are nondeterministic. All specified errors leave state unchanged, which authors state is stronger than RFC 1813. Proving this model does not prove it captures the intended RFC. §4.1 Figure 6: Verified file/directory operations are GETATTR,SETATTR,READ,WRITE,CREATE,REMOVE,MKDIR,RENAME,LOOKUP,READDIR; NULL/COMMIT are verified trivial operations. READLINK,SYMLINK,LINK,MKNOD,READDIRPLUS,ACCESS are unsupported. FSINFO/PATHCONF return implemented constants without specification; FSSTAT has no meaningful specification. No NFS unstable writes or paginated READDIR support is supplied. §5.1: Sequential refinement requires an abstraction relation preserved by every operation Hoare triple, initial-state relation and boundary crash simulation. Mid-operation crash/concurrency reasoning is delegated to transaction correctness. Simulation transfer applies to arbitrary spec programs only if each operation body is both sequentially correct and safe, then wrapped atomically and linked to GoTxn. §§5.1–5.2,9.3: Safe transactions cannot observe/mutate outside shared state through arbitrary global heap access; otherwise replaying the body at commit can change behavior. Two trusted composition assumptions remain: Dafny encoding/transaction semantics correctly imply Coq sequential refinement; every Dafny body satisfies safe. Authors use a simple syntactic mutable-state check rather than a verified cross-language compiler/translation theorem. §§6.1–6.2: Each read/write acquires the corresponding object lock and retains it until commit/abort; disjoint transactions can prepare in parallel and commit batching comes from GoJournal. The linearization point is commit. Abort discards buffered writes. The proof tracks initial footprint J and buffered J′; every accessed address remains locked, and replay from any state agreeing with J on that footprint can reproduce the same partial execution. §§3.2,6.2: Allocator calls are concurrent but do not keep locks until transaction end, so allocation is not transactional atomicity. Its deliberately weak spec can return any value, not necessarily currently free. File system validates allocation candidates against durable bitmap through transaction reads, and updates both volatile allocator and persistent bits on free. This validation preserves safety while neither successful allocation nor progress is guaranteed. §§1,3.2,7.1.1: No liveness or transaction deadlock-freedom proof. GoTxn imposes no global lock order or dynamic deadlock detection. File-system code orders inodes numerically and retries RENAME with discovered inode hints; this described strategy is not a mechanized eventual-completion guarantee. §§3.1,7.1.2: Underlying write-ahead log is 513 blocks; transaction update limit is 511 blocks. Large file operations must stay within limits. Separate ZeroFreeSpace transactions may stop early and are proved to have no visible file-system effect. Their general specification permits arbitrary writes to unused space; the strong verified zero-check is what prevents stale data becoming visible when extending a file. §§7.2–8,9.3: Efficient mutable byte slices and integer-to-byte primitives use 558 lines of trusted Dafny interface specification backed by Go, tested rather than proved. Serialized metadata is updated in place; machine uint64 arithmetic requires bounds/overflow proofs. Reader qualification: Dafny/Coq/Perennial and language/compiler/runtime correctness are toolchain assumptions; this paper does not establish an end-to-end compiler theorem. §8 Figure 12: File-system proof 6787 LOC over 4051 implementation LOC gives about 1.68×, rounded in prose to 2×. Transaction extension alone is 10000/250=40×; reader inference: the prose 20× is consistent with including reused GoJournal 39000/1669≈23×, rather than the extension row alone. LOC ratios are final artifact measures, not proof effort per unit of equally difficult functionality. §§9.1–9.2: Main comparison uses Linux NFS/ext4 data=journal for synchronous durable RPCs; data=ordered log bypass is a weaker-crash-guarantee performance alternative. Both use Linux NFS client. No unstable writes in DaisyNFS. Plot values not numerically printed are saved as approximate visual estimates, and graph claims do not imply equal functionality, production robustness or every workload speed. §9.1: Measurements use Linux 5.15, Go 1.18.1, EC2 i3.metal 72 cores/512GB/local 1.9TB NVMe, restricted to one 36-core socket with turbo/sleep states disabled. Coefficient of variation is reported below 5%; exact repetitions and confidence intervals are not stated. In-memory smallfile parity is prose-only and not graphed. §9.3: fsstress, fsx-linux, Linux/macOS use and all supported two-operation CrashMonkey tests are empirical checks, not exhaustive RFC or crash proof. CrashMonkey found no bugs within that bounded supported suite. Independent collaborator Robert Morris used a wider-range NFS-specific tool; methodology omitted for space. Eleven reported trust/spec bugs show the theorem alone does not validate specification intent or callers. §9.4: One author developed/verified the initial runnable prototype over three months. Four later changes report days and combined implementation/proof LOC, without controlled comparison or independent participant study. No Verus/Rust implementation, TLA+ tool experiment or LLM-agent proof/specification experiment is reported; artifacts/external thesis proofs were not executed. - how much was read: most of it read - source; notes: papers; notes: Verifying the DaisyNFS concurrent and crash-safe file system with sequ - record id: `daisynfs-2022` - Hemiola (2022) - title: Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. - what: A Coq-based language whose templates manage locking, so that invariant proofs consider one transaction at a time. It proves serializability and coherence of MSI/MESI cache models and compiles to Kami hardware. - number: over 10^9 memory requests per protocol in randomized FPGA tests - number: simulations of 500,000 cycles - limits: Verifying the compiler pipeline is future work. FPGA testing is not a general proof of liveness. - how much was read: most of it read - source; notes: Related work absent from the first pass: Hemiola - record id: `hemiola-2022` - Kalas choreographic compiler (2022) - title: Kalas: A Verified, End-To-End Compiler for a Choreographic Language - what: Mechanizes a five-phase compiler from global asynchronous Kalas choreographies to endpoint code and CakeML, composing with CakeML compiler correctness to obtain machine-code guarantees. Proves operational correspondence and network-level deadlock freedom, and deploys a generated producer/filter/consumer system through seL4/CAmkES. Sections 2–3 define asynchronous swapping/deferred-action semantics and endpoint projection, requiring immediate branch notifications when another endpoint’s behavior differs; orphan recursion and divergence introduced at uninvolved endpoints are excluded. Sections 4–6 encode choice as boolean messages, split arbitrary strings into fixed payload chunks with a bookkeeping byte, and convert substitution-based fixpoints into letrec closures, passing variables modified by the body. Section 7 proves weak operational correspondence up to strong bisimilarity with catch-up transitions, then network-level deadlock freedom; local confluence and inert reductions control the interleaving explosion. Section 8 compiles Payload endpoints to CakeML using FFI models, proves FFI irrelevance and forward correctness, and uses proof-producing HOL-function synthesis to discharge each deployment’s environment assumptions. The infinite-execution liveness limitation is discussed explicitly. - number: 5 compilation phases and 2 intermediate languages - number: 3 generated producer/filter/consumer endpoints - number: fixed payload σ>0; transmitted chunks σ+1 bytes - limits: Theorems assume projectable choreographies, all free variables initially bound, well-formed/uniquely named endpoint networks and totally correct CakeML implementations of local HOL functions. Values are byte strings; functions compiled at selected endpoints must be sufficiently executable (no arbitrary Hilbert choice/sets/quantifiers). Communication assumes a live backend, lossless delivery and unbounded queues; payload size σ is positive, chunks are σ+1 bytes. Machine-code liveness is subject to out-of-memory behavior in CakeML. The deployment uses C send/receive glue and seL4/CAmkES IPC, but its proofs are not formally connected to the kernel/platform proofs. Section 8.1 says the current compiler theorem guarantees global progress but does not exclude endpoint livelock for choreographies with only infinite paths; stronger fairness/receive-matching transfer remains unproved. No Internet/TCP deployment or bounded-queue result is supplied. - how much was read: most of it read - source - record id: `kalas-choreographic-compiler-2022` - MET CRDT explorative testing (2022) - title: MET: Model Checking-Driven Explorative Testing of CRDT Designs and Implementations - what: Presents MET, a two-layer workflow that model-checks CRDT designs in TLA+ and turns model-checking traces into deterministic implementation tests. A test manager controls message order through intercepted RPCs and compares code-level state traces with model-level oracles, targeting transcription and assumption bugs that design verification alone misses. The framework specifies CRDT operations and strong eventual consistency in TLA+, then coarsens the model by binding receive/do/send events while preserving conflict-resolution interleavings. Test inputs are extracted event schedules; test oracles are model state traces. A central manager hacks inter-replica RPCs for controllability and adds state-inspection APIs for observability. Practical CRDT-Redis Rwf-RPQ and Rwf-List studies expose a re-add/dummy-position transcription bug, a RemoveWin causal-delivery assumption mismatch, and a position-ID generator bug. The paper reports exact TLC trace counts, disk/time costs, model configurations up to three replicas, and argues from the small-scope hypothesis that three replicas expose most deep conflict bugs. - number: at most 3 server replicas - number: Rwf-RPQ 3–3: 883,413 traces, 1:53 model checking, 20:27 testing - number: Rwf-List 3–3: 5,085,147 traces, 51:05 model checking, 1:46:18 testing - number: Rwf-List 1–5: 69,343,957 traces, 9.64 GB TLC output - limits: The TLA+ network assumes eventual delivery exactly once, arbitrary reordering but no drops/duplicates/forgery, and non-crashing replicas. Coarsening deliberately omits some interleavings; model size is capped (at most three servers, limited requests/attributes) because state explosion is exponential. The small-scope hypothesis is empirical rather than a proof of all deployments, and MET requires manual identification of bug patterns, model/code alignment, test-manager hooks and state-inspection APIs. Tests inspect final states in practice, so unmodeled details and pruned traces can still hide bugs. - how much was read: most of it read - - record id: `met-crdt-explorative-testing-2022` - Refinement of Parallel Algorithms down to LLVM (2022) - what: Adds parallel execution to the Isabelle Refinement Framework and generates verified LLVM. A state-nondeterminism-error monad reports reads, writes, allocation and frees; parallel composition assumes feasible allocation pairs and fails on races. Concurrent separation logic and a VCG prove low-level commands; Sepref refines pure list algorithms to in-place arrays, tracks pointer equalities and splits arrays for disjoint parallel updates. A parallel introsort/pdqsort-style algorithm is proved total-correct and benchmarked against C++. The memory model uses never-reused blocks, so use-after-free and allocation conflicts are detectable. The M-monad invariant requires consistency and an execution avoiding every finite forbidden block set. The disjoint concurrency rule composes Hoare triples; with_split and npar refine independent list subcomputations to same-array disjoint slices. Parallel psort partitions, falls back when depth/size is small or partition is unbalanced, and uses median-of-64 sampling. The final theorem states in-place return of the original pointer and sorted-permutation contents. Generated LLVM is instantiated for uint64 and strings. Figure 2 compares verified, std::sort(par-unseq), and Boost sample_sort over many distributions on laptop/server; Figure 3 shows speedup versus core count. Results are comparable on laptop integers, slower for server strings and highly parallel speedup. The semantics and generated LLVM text remain within an explicit trust boundary: Isabelle’s kernel, the shallow LLVM embedding and the code generator are trusted, and parallel execution uses an external C++ TBB primitive. - number: {'printed_pages': 18, 'server_cores': 22, 'server_ram_GiB': 128, 'laptop_threads': 12, 'laptop_ram_GiB': 32, 'pivot_samples': 64, 'code_width_bits': 64} - limits: Parallel strands must have disjoint or race-free access reports; potential races cause semantic failure. Memory blocks are never reused; each execution allocates finitely many blocks and the model assumes an unbounded supply of fresh blocks (actual OOM is separately defined termination). The framework targets a small LLVM fragment, multicore CPUs and a parallel combinator; locks, atomics, read-only fractional ownership and GPUs are future work. Sorting correctness assumes a weak ordering and array length represented by a fixed-width word; code generation fixes widths to 64 bits and uses an int64 size signature. Benchmark evidence is runtime comparison, not a proof of speed or broad hardware scalability; no distributed network model, Rust/Verus, TLA+ or LLM agent is evaluated. The trusted code base includes Isabelle’s inference kernel, the shallow embedding of a small LLVM fragment and the text code generator. The parallel primitive calls an external C++ implementation using tbb::parallel_invoke. Correctness is proved against the embedded semantics; the paper does not prove the LLVM compiler, TBB runtime or complete LLVM-to-binary toolchain correct. - how much was read: most of it read - - record id: `refinement-of-parallel-algorithms-2022` - Taming Armv8 (2022) - title: Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification - what: Connects a compact L3 Armv8 specification to a HOL4 model extracted from Arm’s authoritative Armv8.6 A-class ASL specification via Sail and Lem. Instruction simulation lemmas then support a CakeML compiler correctness theorem with respect to the ASL-derived machine semantics. Sections 3–4 explain the extraction pipeline, manual patches and proof engineering needed for a 488 kLOC HOL4 specification. The authors replace set-valued nondeterminism with Hilbert choice, replace address translation by an identity map and widen physical-address types. The state relation aligns common registers and memory under system-register and well-formedness constraints; l3_models_asl requires allocated decoding and successful exception-free L3 execution. Symbolic evaluation bypasses monolithic ASL decoding before interactive proofs for arithmetic, logical, branch, address and load/store instruction classes. The simulation takes 7.5 kLOC proof plus 0.5 kLOC automation. Section 5 reuses CakeML’s L3 encoder and runs Asm, L3 and ASL state machines together to establish instruction and whole-program results. The final theorem permits resource-limit failures. The work reproduces a known cbnz/cbz error and validates its correction; CakeML does not emit cbnz. - number: ASL 168 kLOC source → 488 kLOC HOL4 - number: L3 2.4 kLOC source → 8.5 kLOC HOL4 - number: ASL extraction ~2 h, build ~3 h; L3 extraction ~1 s, build <30 s - number: 7.5 kLOC instruction proofs + 0.5 kLOC automation, ~40 min build - limits: The theorem covers the supported general-purpose instruction subset under explicit system-register constraints, a well-formed state, encodeability and appropriate compiler/machine configurations. Address translation is stubbed, and the machine stepping model omits interrupts and devices. The proof does not cover all Arm features, exception behavior or hardware concurrency. Official ASL is the root of trust; ASL→Sail→Lem→HOL4 extraction is unverified and includes manual changes. The paper suggests testing generated HOL4 against Arm tests or hardware as future validation. Whole-program machine behaviors refine source behaviors extended with out-of-memory errors. - how much was read: most of it read - source - record id: `taming-armv8-2022` - Yuen capstone (2022) - title: Verifying Distributed Protocols: From Executable to Decidable - what: This capstone studies translating TLA+ distributed-protocol models into Ivy so that finite model checking can be replaced by sound decidable verification. It gives computer-aided TLA+ and Ivy verification case studies for Suzuki–Kasami mutual exclusion and a substantial part of NOPaxos, and sketches translation rules. - number: Verdi Raft is cited as over 50,000 proof lines for 500 implementation lines (p.2 footnote) - number: Suzuki–Kasami TLA+ model checks one mutual-exclusion safety property plus eight supporting invariants (pp.15–16) - number: Suzuki–Kasami Ivy proof uses five conjuncts in an inductive invariant (pp.19–20) - limits: The work verifies abstract protocol models, not deployed Rust or Go implementations. The translation is only a framework sketch; the report says some TLA+ features and liveness details still need manual re-expression. - how much was read: most of it read - source - record id: `yuen-capstone-2022` - Cameleer: A Deductive Verification Tool for OCaml. (2021) - what: Translates GOSPEL-annotated OCaml programs to WhyML and invokes Why3 verification-condition generation and SMT solvers. Extends GOSPEL from interface contracts to implementation annotations including loop invariants and ghost code. Supports a bounded-mutability subset with basic modules/functors; reports a26-case verified gallery. Proof success concerns supplied specifications and translated semantics,conditional on front-end/solver correctness and assumptions. Shows higher-order and functor binary search with loop variants and exceptional postconditions;maps OCaml attributes,ghost code,type invariants and module namespaces into WhyML. Integrates OCaml as a Why3 input format using the Why3 API/session tools,and uses extraction to erase ghost code. Explicitly documents rejection of recursive mutable Queue cells under Why3’s alias discipline,and gives line counts,VC counts,replay times and manual-interaction flags across realistic library fragments and textbook algorithms. - limits: Programmer supplies contracts,invariants,termination variants,ghost functions and sometimes manual auxiliary induction/case splits. Discharged VCs prove those formal requirements,not that the requirements express all intended behavior. Axioms in module signatures constrain admissible implementations and must be justified at instantiation. Cameleer trusts its GOSPEL parser/type-checker and OCaml-to-WhyML translator,Why3 typing/effect analysis/VC generation and external solvers. The paper refers to inductive translation rules in the longer report but does not present a machine-checked compiler/refinement correctness theorem in this chapter. Higher-order comparison arguments used in specifications are assumed pure. WhyML’s bounded-mutability discipline requires aliases to be statically known. Effectful higher-order code and recursive mutable data types are limited;arbitrary OCaml pointers/aliasing are not handled by this translation. Supported subset roughly corresponds to caml-light plus basic modules/functors. Objects,GADTs and polymorphic variants are unsupported. Viper/CFML integration and richer heap reasoning are future work in this2021paper,not implemented capabilities established by the case studies. Source integer overflow and precise machine-integer correspondence are not explained in the supplied chapter. Do not infer that mathematical arithmetic VCs automatically prove every OCaml machine arithmetic corner case without checking library models and translation. Case-study proof replay is measured after contracts,lemmas and proof sessions have been developed. “Immediate” means no extra IDE interaction after annotation,not no human proof design. Manual sessions are retained for six cases. No failed-case population,annotation time or developer-effort study is reported. Quoted comparison of tool usability/language suitability reflects author opinion and2021tool scope. Related-work mentions Prusti and Tezos proofs in other tools;neither is an evaluated Cameleer Rust/blockchain case. - how much was read: most of it read - source - record id: `cameleer-a-deductive-verification-2021` - everquic (2021) - title: A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer - what: EverQuic has two parts. The record layer is in F*/Low*, proved memory safe, functionally correct and cryptographically secure, and extracted to C. The transport is in Dafny, proved memory safe and type safe, with no integer overflow and local termination. - number: about 10K F* lines / 6K extracted C; 10K Dafny / 13K C++ - number: about 20 person-months including training - number: Fig 9: transport 10,223 lines, 19m46s; record layer 9,836 lines, 16m30s (component rows exceed the printed total) - number: 1.98 GB/s at 1300-byte MTU; small transfers about 2x slower, large about 21% slower than ngtcp2 - limits: It is not end-to-end protocol verification. It has no proof of eventual delivery. The payload offset is declassified, which may leave a cache side channel. - how much was read: most of it read - source; notes: Related work absent from the first pass: verified QUIC record layer (2 - record id: `everquic-2021` - GoJournal: a verified, concurrent, crash-safe journaling system (2021) - what: GoJournal provides concurrent, crash-atomic journal operations for Go storage applications. Perennial 2.0 (Iris/Coq) proves its implementation with layered logically atomic crash specifications, ownership lifting, crash-aware locks and crash framing. SimpleNFS demonstrates a verified restricted NFS client application; unverified GoNFS supplies performance/functionality evidence. The proof makes operation preparation sequential and crash-free while retaining explicit locking/commit/recovery obligations. Records the local/durable predicate transfer and commit failure/crash outcomes, post-crash resource generations, ReadBuf wand/dirty requirement, logical-log boundaries and lower-bound abstraction, lock-free stale-block invariant and header callback. Includes every LOC/proof cell, concrete absorption race/fix, slow-SSD/scalability failures, benchmark/configuration asymmetry and complete artifact appendix rather than treating fast-NVMe throughput as a universal result. - limits: §4: Disk reads/writes are synchronous atomic 4KB sectors, including crash-time atomicity. Executable code must follow Goose-generated Perennial semantics; the paper assumes this correspondence. Arbitrary execution/recovery crashes are modeled. Hardware, compiler/runtime, translation correspondence and proof checker remain in the trust argument; this reading did not independently audit or rerun them. §§1,3.1,4: Journal operations do not implement automatic concurrency control. Caller must exclusively own/lock every accessed object, including reads, until completing its use. SimpleNFS proves its locking; functional GoNFS is unverified and its locking is trusted even to obtain atomicity, and that trust alone says nothing about full NFS conformance. No theorem transfers SimpleNFS correctness to GoNFS. §§1,5.6 fn3,8.1: Internals implement deferred durability and lower-level specifications can express Commit(false), but the presented top-level separation-logic API requires immediate flushing with Commit(true), sufficient for SimpleNFS. Main performance evaluation uses stable GoNFS writes although Linux can exploit unstable writes. Separately reported unstable-write rerun and appendix comparison are distinguished. §§1–2: No floating commit blocks, database-style undo, asynchronous-disk/log-bypass optimization or sophisticated B-epsilon-tree data structure. Objects must fit supported operation sizes; Commit can fail if operation is too large. Abandoning an uncommitted buffered operation is a logical ownership restoration, not undoing an already journaled operation. §§3.1,5.1: SimpleNFS is a core subset with GETATTR, SETATTR, READ and WRITE examples, not a fully verified NFSv3 implementation. Each file occupies one block; writes reject count/data-length mismatch, arithmetic overflow, beyond-block size and a starting offset beyond current EOF. Inode and data block must update together; per-inode locking owns its uniquely associated block implicitly. §§4–5: Hoare triples establish safety and postconditions if calls terminate; these are not stated liveness, fairness, deadlock-freedom or throughput guarantees. Toy-client idempotent recovery specification covers arbitrary crash/recovery repetitions within the model, not guaranteed completion under endlessly recurring crashes. §5.2: Lifting changes ghost ownership, not physical disk. Operation-local ownership permits access while durable_pred snapshots the original footprint. Exclusivity applies only to owned objects; other threads may commit changes elsewhere, including disjoint objects sharing a block. Whole-disk immutability throughout an operation is not assumed. §§5.3–5.5: ReadBuf returns mutable-buffer ownership and a separating implication to recover the operation predicate with the new contents. Footnote2 omits the actual SetDirty obligation from the displayed simplified spec. Crash-aware lock clients must preserve next-generation durable recovery obligations during every critical-section step; ordinary lock release invariants alone are insufficient. §5.5: Crash framing removes access to crash-resource Ic during proof of f and restores it afterward. It does not allow arbitrary durable-state mutation to ignore its crash consequences. Operation preparation uses only local buffered resources while the original durable footprint is framed away. §§6.1–6.3: Lock-free describes selected reads/disk-I/O regions; commits serialize read-modify-write under a global lock, and logger/installer take locks to obtain monotonic bounds. No general lock-free progress theorem is claimed. Separate header ownership allows concurrent installation/logging without holding locks during I/O. §7: Authors report all Perennial/GoJournal/SimpleNFS proofs Coq-checked and Print Assumptions used to check completeness. The article supplies specification rules and proof ideas rather than full in-paper derivations. Public artifacts were not replayed here, so this record distinguishes reported machine checking from independent reproduction. §8.1: Performance uses unverified GoNFS against Linux5.12.3 NFS/ext4 data=journal; RAM backing differs (Go array versus ext4 file in tmpfs). Desktop XeonE5-2640 20cores2.4GHz/64GB/Samsung850PRO256GB and i3.metal72vCPU/512GB/1.9TB NVMe; one socket, turbo/sleep/Spectre mitigations disabled. No run counts, confidence intervals or variance bars are specified in the main results. §§8.1–8.2: At least90% claim is for these workloads on RAM/NVMe and smallfile/app on SSD; stable largefile on slow SSD falls below20%. Linux exploits unstable writes whereas stable GoNFS serializes same-inode writes and flushes64KB batches. NVMe scalability advantages are not causally isolated; authors offer possible design differences. SSD GoNFS batching limits scalability after about7clients (prose says cores, axis clients). §§8.3–8.5: 44/462 code lines needing crash reasoning and proof:code ratios are empirical source-structure proxies, not a controlled human-effort study or time measurement. WAL/JRNL STS and ownership abstraction rows share implementation code, so their printed merged ratios combine proof rows. Framework20,260Coq lines are additional to application/library proof counts. Appendix A.1–A.6: VM artifact reproduces LOC tables and selected plots, not every expanded main-paper graph. Main performance evaluation was expanded after artifact review. VM results use MacBookPro i9-9980HK2.4GHz/8hostcores, VirtualBox4cores/8GB with0.4ms barrier, so differ from carefully controlled physical machines. Pre-generated Goose model is included along with regeneration instructions; its presence is not a proof of translator correctness. §8.3/figures2–3: Printed reference to Figure3 lines6–8 for lock acquire/release actually matches Figure2. Figure2 uses txn.Commit despite naming the local variable op; §5.7 prose starts Begin before acquire while code acquires first. Reader treats these as presentation inconsistencies, not evidence the checked source has those exact errors. No Verus, TLA+, Rust implementation or LLM-agent evaluation is performed. §7 Figure12: Printed Go component rows sum to1,347 (109+555+133+121+118+311), while printed GoJournal total is1,345. Both transcribed as printed; proof rows sum correctly to25,797 and framework rows to20,260. No source correction is inferred. - how much was read: most of it read - source - record id: `gojournal-a-verified-concurrent-2021` - The CakeML Project’s Quest for Ever Stronger Correctness Theorems (2021) - what: Historical account of CakeML’s end-to-end verification strategy: proof-producing translation of logical functions to embedded ML programs, verified compilation to concrete bytes, and application-specific proofs, with extensions through a verified Silver CPU’s Verilog implementation. Describes improvements that strengthen transported correctness, especially impure code reasoning and space bounds needed for liveness. Explains why in-logic execution supplies a concrete compile(input)=machine_code theorem, enabling a final property statement without the compiler function; how applying synthesis and in-logic compilation to the compiler’s own logical definition yields a verified executable; why finite target memory limits the default behavior theorem; how a sound space-cost semantics removes early out-of-memory exits for specific programs; and how shared characteristic-formula infrastructure connects manual verification and monadic code synthesis. Separates completed compiler/hardware layers from 2021 prospective language/compiler projects. - limits: This 10-page invited overview summarizes previously published mechanizations; it contains no new complete formal proof, benchmark table, theorem inventory or fresh controlled experiment. Its references identify where to inspect the underlying statements. Counts or broad performance comparisons here are author reports, not independently reproduced results. The transfer argument relies on proved source properties, formal CakeML operational semantics, a correct compiler theorem and a proved concrete compilation result. In-logic compilation removes the compiler from the final statement; it does not eliminate trust in the logic, prover implementation or fidelity of source/machine/hardware models. Source lists, arrays and integers are unbounded; target memory is finite. The default behavior preservation explicitly permits early out-of-memory errors. Source liveness alone therefore does not ensure target liveness. The separate compiler-sound space-cost semantics supports tight bounds for concrete programs and the strengthened transfer. The first compiler’s front end includes parser soundness/completeness with respect to an SML syntax grammar, type-inference soundness (completeness added later), and no runtime errors for typed source programs. That typing theorem does not rule out target out-of-memory exits. The optimizing compiler uses eight intermediate languages and multiple passes per language. Functional big-step, clocked interpreter semantics permit a single simulation proof per phase to handle termination and nontermination; the paper says most, not all, simulation directions are forward. CakeML characteristic formulae are proved sound against CakeML operational semantics, including higher-order recursive functions, mutable state, exceptions and FFI I/O. A later extension handles diverging programs, and a simplified nontermination Hoare logic is proved sound and complete. Do not extend that completeness claim to every CF feature or program-verification automation. The Isabelle/HOL source generator is for the most part verified once for all; the HOL4 generator is for the most part proof-producing. Lem generates source-semantics definitions in both provers from a common specification. The overview does not present a verified cross-prover transport theorem or certify Lem itself. The Silver result composes a verified compiler target, machine-code filesystem and CPU correctness through the formal Verilog implementation. A later verified compiler maps a supported subset of generated Verilog to FPGA technology-mapped netlists. Physical fabrication, FPGA programming and the entire external synthesis toolchain are not established by this overview. Compiler projects using CakeML for a low-level imperative language, a Haskell-inspired language and a choreographic language are described as ongoing in 2021. Project-success explanations are explicitly the author’s beliefs, not empirical causal conclusions. No Rust, Verus, TLA+ or LLM-agent experiment is reported. - how much was read: most of it read - source - record id: `the-cakeml-project-s-2021` - Aneris (2020) - title: Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems - what: Aneris is a Coq-mechanized higher-order distributed concurrent separation logic for modular specification, partial correctness and refinement; the repository contains examples and case studies. - number: load balancer impl/spec/proof 18/78/95 lines - number: two-phase commit: 18 and 11 impl lines, 181 joint spec lines, 265 and 280 proof lines - number: replicated logging plus commit: 1,272 lines - limits: README-level account; publications linked from the README are separate sources. - how much was read: most of it read - source; notes: papers - record id: `aneris-2020` - Aragog (2020) - title: Aragog: Scalable Runtime Verification of Shardable Networked Systems - what: Operators write patterns of bad event sequences. Aragog compiles them into state machines and checks them against live or recorded event streams from networked systems. It splits the work by grouping keys. - number: 8 NAT policies at 5-14 spec lines, 3 firewall policies at 4-6 lines - number: four bugs in the NAT gateway, confirmed by operators - number: over 500,000 events/s for one policy, over 30,000 for eight - number: firewall violation detected in about 70 ms median - limits: Aragog has no correctness proof. It needs accurate event ordering and synchronized clocks. Sampling can miss flows. Operators write the specs. - how much was read: most of it read - source; notes: Aragog: Scalable Runtime Verification of Shardable Networked Systems; notes: Aragog: Scalable Runtime Verification of Shardable Networked Systems - record id: `aragog-2020` - Armada (2020) - title: Armada: Low-Effort Verification of High-Performance Concurrent Programs - what: Armada is a language and tool for formally verifying high-performance concurrent programs using SMT automation, rely-guarantee, TSO elimination, reduction and alias analysis. Its README describes four case studies and build commands. - number: 4 concurrent case studies - number: barrier: 57 executable SLOC; second layer 35 annotations, 114 lemma lines, 46,404 generated proof lines - number: four cases: barrier, distinct-pointer reorder, MCS lock, liblfds queue - number: about 6 person-days to write the proof levels for one queue, mostly finding the inductive invariant (§6.4, PDF p.12) - limits: README describes a PLDI paper and commands; no local build was run. - how much was read: most of it read - source; notes: Armada: Low-Effort Verification of High-Performance Concurrent Program - record id: `armada-2020` - Automated Verification of Customizable Middlebox Properties with Gravel (2020) - what: Gravel checks high-level trace properties of Click middleboxes in two stages: symbolic graph execution over Python element specifications, then LLVM symbolic execution/refinement of each C++ element against its specification. Run-to-completion handlers, restricted pointer analyses, loop unrolling, SMT models of Vector/HashSet/HashMap and concrete immutable classifier rules make most studied elements encodable. Developers still supply the high-level properties, intermediate element models and induction obligations. Records exact empirical screen/failure classes, graph-versus-element obligations, bounded graph/unrolling failures, SMT model/trust/init limits, explicit liveness/induction formulas, all13propertyscopes and full appendix examples/discrepancies, complete LOC/time/bug/performance cells and workload/selection limitations. - limits: §§2,3.1: Study is run-to-completion Click elements/configurations in official repository, not arbitrary concurrent network software. Element private state/event handler semantics and fixed directed topology underlie composition. Packet/time events modeled as state transitions; no shared-memory concurrent handler/interleaving proof or distributed consensus/failure model is presented. §2/Table1: Percentages measure ability to symbolically encode examined code after techniques/modifications, not verified high-level properties for226elements/37configurations. Baseline uses conservative no-pointer/no-loop criteria; later supports immutable unaliased singleton/array pointers, staticbounds, byte-valued uninterpretedfunctions and boundedunrolling. Error at limit is failed verification, not bounded-prefix success. §§2.3,4.2/AppendixA: Vector/HashSet/HashMap implementations replaced by SMT interface models. Paper supplies encodings rather than refinement proof of those underlying library implementations; their faithfulness/implementation correctness is an additional assumption despite terse §4.3TCBlist. Arbitrary recursive/custom datastructures unsupported. Generic payloadloops/AES andsymbolicstate-dependentloops remain obstacles. §2.3: Classifier rules are instantiated from concrete Click configuration; verifier checks transitiontableimmutable and symbolicallyprocesses packets with those fixedrules. This is configuration-specific verification, not a theorem for arbitrary ruleconfigurations or mutablepolicyupdates. §§3–4: High-level spec and element-level specs required. Element models are checked against LLVM so not simply trusted, but abstract operations/runtime and packet/state representation relation remain trusted. Compilation frontend/LLVM/back-end toolchain and Python/Z3/Clickruntime are inexplicitTCB. No verifiedNIC/OS/DPDK/hardwarestack. §4 Theorems1–2 are checker obligations: graphcomposition meets suppliedhighlevelproperty; each concretepossibletransition has counterparts in elementmodel. Paper describes symbolicchecks, not mechanized metatheory proving wholeverifier sound. Counterexamples dependonfaithfulmodels;specificationadequacy remainshumanobligation. §§3.3,4.1: Property1 calledliveness is immediateTCP-input→nonnull-outputcondition on terminatinghandler. It is not fair-scheduler/eventualdelivery/failure-recoveryliveness. Unboundedtrace persistence instead uses explicitbaseandpacket/timepreservation obligations; no bound on numberofevents if inductionvalid. Graphcycles allowed but maximumtraversal capmustsuffice (ToyLB6); hittingcap rejects. §5.3/Table3: Initialization assumedcorrect; malformedconfigurationcrash excludedfromguarantee. Paper does not prove construction/boot/configuration parser correctness. Bitvectorpacket/time/countersemantics and any time-wrap/monotonicity/precondition adequacy mustmatchspec; no general real-time guarantee beyondwrittenformulas. §5.1: MazuNATRFC5382properties omitICMPbecauseunsupported. Showingselectedmapping/filtering/hairpinning/memorization/payloadproperties is not fullRFCcompliance. Roundrobin andMaglevLB are bothdiscussed;fiveTable2applicationrows not anenumerationofeverypossibleLBvariant. §5.3: OriginalMazuNATendpoint-independence mismatch found/fixed is actualverificationfinding. Table3is manualassessmentofexistingbugreports/CVE-relatedsearch,not replayedinjectedbugsuite. Authorsscreen30recentbugs,exclude20 (10unsupportedfeatures,3docs,5CLI,2performance),thenclassify7/10preventable. Cannotgeneralize7/10toallbugs orclaim30experimentallycaught. §5.4/Table4: FiveconcurrentTCPflows/iperfthroughput,NPtcp200byteRTT,twohosts40Gbps,not saturatedsmallpacketMpps/adversarialstatechurn/largeflowcountbenchmark. ±values areprintedwithoutdefinedsamplecount/statistictype here. NATmeanRTT14.43→15.14us (~4.9%increase),soauthornegligibleoverheadclaimdoesnotmeanalllatenciesidentical. Replacingpriorityqueuewithlinearscanmayhaveunmeasuredscalingcost. §1/Table2: Introapplicationsequence assigns1151LOC/70highlevelLOCtoloadbalancer and1447/68tofirewall;Table2labels1151/70asFirewalland1447/68asLoadBalancer. SavedTable2labels asprimarystructureddata andnotedsourcediscrepancy. §3.4,p.229/AppendixA,p.236: Prose/filterexample saysremoveallmatchingpredicateentries, butAppendixAprintsnewcontain(k)=p(k,fvalue), withneitheroldcontainconjunctionnorpredicatenegation. mapformulaalso passesfvalueratherthanexplicitfvalue(k). Sourceequationsretainedasdiscrepancy; noimplementedunsoundnessallegationwithoutartifactcheck. §§3.2–3.3/AppendixB: ToyLBproseusuallyrewritesdestination,butProperty1callsencapsulated andappendixnewflowusesinner_ipwhileknownflowusesip4. MainpropertycodeprovesnonnullTCPoutput,notexactencapsulation. AppendixCmemorizationusesc/steer_towithdefinitionnotincluded andbasecreatesp1unused;printedexamplesalonearenotverifiedartifactreproduction. §6: Specificationsstillrequirehumaninduction/designdespiteautomatedsolverchecks. NoVerus/verifiedRust,TLA+,LLM-agentorwhole-networkroutingloopresult;non-Click/XDPextensionisproposedpossibilitynotimplementedmeasurement. - how much was read: most of it read - source - record id: `automated-verification-of-customizable-2020` - Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer (2020) - what: SCFTL implements a sequential read/write/flush disk interface whose completed flush commits a snapshot. Ordinary crashed operations preserve the last snapshot; a crashed flush may retain the prior snapshot or commit the new one. Stable logical-to-physical mapping uses committed delta pages/full checkpoints, and two-phase GC retains snapshot data until flush. Agda establishes the abstract simulation framework; Serval/Rosette/Z3 verify implementation obligations with manual transformations and three verified runtime validators. FEMU and modified xv6 benchmarks examine flush-frequency tradeoffs. Records precise crashed-flush nondeterminism and repeated-recovery semantics, no-op write bounds and upper-layer obligations, all five checkpoint recovery cases, GC capacity inequalities, four state/abstraction relations, SMT overapproximation/ghost/partition techniques and proof gaps. Saves all LOC cells, size-specific verification times, partial-data stress-check scope, exact filesystem labels and adverse high-flush/ext4 comparisons. Separates mathematical metatheory, solver checks, validation and unverified upper layers. - limits: §§1,4.2: Deterministic recovery refers to a crash during a regular operation after the last successful flush. A crash inside flush can recover either the old snapshot or the new pre-flush volatile state. The abstract specification explicitly permits both; no unique snapshot independent of crash position is promised. Repeated crashes during recovery preserve the stable state until a successful recovery. §§3.2,4.1 Figure 4: Writes outside address/counter bounds are no-ops. InBounds uses a≤amax and wcnt≤wcntmax; the counter increments after an accepted write, so exact boundary interpretation follows that inclusive condition. Upper layers must budget every atomic operation before execution, flush before insufficient capacity and split an operation larger than a whole epoch. A flush midway could persist a partial operation. §§1,6.2: Top-level SCFTL operations are sequential; concurrent FTL requests are unsupported by specification/proof. Flash commands inside or across successive unsynchronized operations can overlap and reorder across pages until SYNC. Hardware parallelism is distinct from concurrent client-operation verification. §§2,4–6: Agda mechanizes the disk/simulation metatheory; C implementation obligations are symbolically evaluated with Serval and discharged in Z3. Manual reformulation/partition of obligations is connected by pen-and-paper reasoning, explicitly leaving a gap in the formal proof. Do not call the whole C-to-snapshot proof one continuous machine-checked derivation. §§6–6.1: Three properties are not proved for the main implementation: injective L2P after recovery, enough space after recovery and enough space after flush. Verified validators establish success-flag⇒property and may only change validation variables. No notification occurred in experiments; that does not prove the implementation always satisfies these properties or always continues successfully. Failure notification is not a demonstrated recovery/fallback for these three checks. §6: TCB assumes error-free flash; correct Z3, Agda and Serval; correct LLVM-to-machine-code translation; correct LightNVM Linux module. Hardware/media faults, bad blocks, wear-out and ECC failures are outside the guarantee. No hot/cold separation or wear leveling implemented; validator-checked unverified allocator is an example of a possible extension. §§3.1,5.1: Model has erase-before-write/sequential page constraints, same-page command ordering and arbitrary cross-page scheduling. READ returns the latest modeled content irrespective of sync flag; normal I/O semantics assumes this behavior. Unsynchronized crash pages are overapproximated as arbitrary values, not enumerated physical histories. This is conservative for crash reasoning within the assumed command semantics. §§3.3–3.4: L2P is the persistent primary data; P2L/queues/counts rebuild after recovery. Invalid blocks may still hold stable-snapshot sectors, so they become erasable only after flush. No internal flush is allowed merely to facilitate GC because it would change the externally selected snapshot. Capacity bounds and reserved space are part of the implementation contract. §§4.2–4.4: Behavioral correctness compares reads in normal states following successful operations; crash states need only weaker CR/CI. Initial new disks must recover before use. Lemma 1 proves the abstract disk snapshot-consistent; Theorem 1 derives observational simulation from initial relations/per-operation Type A and invariant Type B obligations; Theorem 2 transfers snapshot consistency. These safety properties do not establish termination under arbitrary permanent crashing or concurrent request semantics. §§5.2–5.4: Ghost arrays remove existential choices while non-ghost transitions remain independent. Splitting postconditions and dropping antecedent conjuncts strengthens obligations; proof partition manually maps crash states to old/new flush outcomes. Fast solver checks still require correct semantic construction and checked side conditions; absence of one timeout is not completeness for all capacities. §6: Verification instantiates one capacity at a time: reported 8GB and 256GB results and selected write bounds 2048–20480. It is not a universally quantified theorem for all device sizes/configurations. Counts are 98 RI/AR and 17 CI/CR conditions; they are not 115 independently complete correctness properties. §7: Performance runs on FEMU/QEMU emulated Open-Channel SSD, Linux 4.15, liblightnvm/libaio with added NVMe base-command latency emulation. Not a physical SSD endurance/power-cut evaluation. Host is printed as 12-core i7-8700; retain source label without independently correcting core/thread terminology. §7.1: Stress tests compare only first few bytes of every sector; four configurations/eight hours, over 1.4TB writes, about twelve million flushes and ten thousand simulated crashes. Garbage on unsynchronized pages tests a modeled failure behavior. Passing these checks is not exhaustive byte-level recovery validation or proof that real hardware obeys the model. §7.2: async baseline does not do checkpointing and omits 2PGC and write bounds. sync uses synchronous commands and an assumed battery-backed merge page, ignoring flush. pblk receives one-thread/four-thread tests while SCFTL stays sequential. These have unequal crash guarantees and concurrency; performance ratios are conditional tradeoffs. §7.3: xv6 changes are unverified demonstration code; extending proof to upper layers remains future work. xv6-group persists through fsync and allows later system calls to roll back as a prefix, whereas comparison xv6 variants provide immediate durability at every syscall. The speedup combines lower flush frequency, log removal and changed durability timing; it is not an equal-durability implementation-only gain. §7.3 Figures 7–8: Main headline says 3–30× and at worst two times slower, but rounded printed largefile labels give 39/0.6=65× versus xv6/async (32.5× versus sync), and SQLite 142/61≈2.33× slower than ext4-data. Preserve exact labels and identify approximate headline wording rather than force agreement. Largefile Figure 7 group bar exceeds chart top; use printed 39MB/s rather than bar height. §7.3: Five runs per filesystem workload, reported standard deviation under 8%; this statement does not supply raw runs or certify every FTL/boot measurement used five repetitions. mailbench on ext4-metadata adds fdatasync to its temporary file. Benchmark-specific sync protocol/configuration matters for fairness. §§2,8: Verified layered storage, concurrent FTL operations and commercial optimizations remain future work. Relevant to crash specifications and agent proof evaluation, but no Verus/Rust, TLA+, LLM-agent study or distributed-consensus theorem. Saved PDF contains no artifact appendix/repository pointer; no external implementation or proof replay. - how much was read: most of it read - source - record id: `determinizing-crash-behavior-with-2020` - Igloo refinement bridge (2020) - title: Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification - what: Introduces Igloo, an Isabelle/HOL framework connecting compositional event-based distributed-system refinement to code verification in expressive separation logics. Sound refinement and trace inclusion let protocol proofs transfer to heterogeneous Java/Python implementations verified by VeriFast and Nagini. The framework proves composition and translation theorems for event systems, I/O specifications and process implementations. Case studies cover leader election, primary-backup replication and two-party authentication, including fail-stop servers, TCP, UDP, cryptography and unbounded component instances. Isabelle formalizes all definitions/results; code-level abstraction functions connect model states to locked heaps and message bytes. - number: Three complete case studies - number: Primary-backup proof uses nine invariants for backup consistency - number: Java and Python implementations verified with VeriFast/Nagini - number: All definitions and results mechanized in Isabelle/HOL - limits: Correctness depends on explicit environment/fault assumptions (perfect failure detection, channel guarantees, Dolev–Yao abstraction) and trusted library contracts/parsers. Implementations are manually written Java/Python; extraction is not automatic. Security bitstring cryptography is abstracted through a surjective abstraction function and trusted cryptographic libraries. - how much was read: most of it read - source; notes: papers - record id: `igloo-refinement-bridge-2020` - tlaplus-monitor (2020) - title: ONOS TLA+ Conformance Monitoring Tools - what: A customized TLC deployed with Helm. It reads JSON traces from Kafka, updates the model state, and checks TLA+ invariants that users write. It has optional sliding windows. - number: one monitor pod per TLA+ specification - limits: There is no paper, and no bug counts, throughput, size or effort. It checks safety invariants on observed traces only. In the documented example, the predicate accepts decreasing versions despite its comment. - how much was read: most of it read - source; notes: ONOS TLA+ Conformance Monitoring Tools - record id: `tlaplus-monitor-2020` - VeriBetrKV (2020) - title: Storage Systems are Distributed Systems (So Verify Them That Way!) - what: VeriBetrKV verifies a single-threaded crash-safe B-epsilon-tree key-value store by combining ordinary Hoare code proofs with TLA-style state-machine refinement of program plus asynchronous disk environment. Reusable crash-safe/cache templates and transposition split journal and tree reasoning. A Dafny linear/shared extension coexists with dynamic frames and a trusted C++ backend; case studies measure reduced proof annotations and competitive but uneven performance. Records disk acknowledgment/corruption/sync contracts, full refinement decomposition and disjoint-region condition, linearity/BoxedLinear trust and borrowing rules, checkpoint/journal architecture, proof-latency discipline and its empirical caveats. Saves complete code/proof tables and printed benchmark values, including contradictory speedup and latency prose. Separates a general asynchronous-system method from an actual multi-node or CPU-concurrent implementation. - number: Table 1: 1210 spec, 6373 implementation, 44685 proof lines; the crash-safe map spec is 283 lines - limits: §§1–3: Safety and functional correctness only; operations need not terminate. Implementation is single-threaded, with asynchronous I/O/pipelining but no CPU concurrency. Demonstration has one processing node and one disk. Multi-node/multi-disk/heterogeneous generalization is conjectured, and shared-memory thread concurrency is future work. IronFleet has distributed/liveness results, but those are prior work, not VeriBetrKV results. §2.1: User trusts a 283-line top-level dictionary/crash contract, environment/OS/runtime API specifications, build system, modified Dafny/verifier/Z3, C++ backend/compiler/toolchain and hardware behaving as modeled. Smaller specification size may aid review but does not prove the specification matches intent. The linear typechecker changes and BoxedLinear primitives are trusted rather than a separately proved compiler/type-system soundness theorem. §§2.1,3.1: The I/O bus can reorder requests/responses but cannot duplicate or drop them except during crash. The composed StorageIOSystem nondeterministically takes a program step, disk/environment step or whole-system crash. Crash resets volatile program state; acknowledged writes survive, while unacknowledged addresses may contain old, new or corrupt bytes. Arbitrarily many crashes at arbitrary modeled points are covered, including reboot/recovery states. §3.1.1: Disk corruption can occur at any time but cannot produce a valid-checksum block. CRC32C is trusted and referenced by the disk model. Invalid checksum aborts the current query, preserving no-wrong-answer safety at the cost of availability. A malicious disk that fabricates valid checksums, checksum collisions or stale valid blocks violates the assumed model. This is not an unconditional CRC integrity guarantee or fault-tolerant recovery from arbitrary corruption. §§3.1.2,6.2.3: Without crash/corruption the visible state is a dictionary with latest writes. Crash reverts the entire dictionary to a consistent prior snapshot no earlier than the last completed sync. Spec has ephemeral and persistent states; background steps can advance persistence. sync_start/sync_end ensure that at end, persistence includes the state at start or a newer version. Unsynced operations may survive or disappear as part of a consistent snapshot; this is not independent per-key arbitrary rollback or durability of every returned insertion. §3/§6.2: Hoare reasoning verifies synchronous local implementation handlers against the program machine. Environment behavior and crashes are handled by IOSystem refinement. General real-system theorem is conditional on the actual executable, trusted API interactions and environment matching those models. TLA-style refinement is encoded/proved with Dafny, not reported TLC model checking or proof of arbitrary storage behavior. §§3.2,6.2.2: Map→abstract B-epsilon tree with infinite-map nodes→finite pivot-bucket tree separates key semantics from representation. A hypothetical purely in-memory implementation is shown gray and is not an actual second implementation. Generic CrashSafe<T>/BlockCache<T> lifting says a refinement of node/tree contents lifts through a crash-safe cache/disk composition. §6.2.3 Figure 3: Tree IOSystem and JournalIOSystem independently refine CrashSafe<Map> and JournalViewMap. CompositeViewMap applies journal operations to map snapshots. ConcreteCache adds byte marshaling; Disk<byte> refines a partitioned typed disk. Transposition rearranges program/environment components only with an invariant that tree and journal access mutually disjoint disk regions. Their models cannot simply be separated if their effects overlap. §6.2.4: Executable handler invocations refine Next transitions of ConcreteCache; I/O labels are no-op, request or response and must match trusted API actions. Proving code-to-model is insufficient without the enclosing disk composition, while proving abstract crash safety is insufficient without this implementation connection. Recovery does not write disk (§8.1), avoiding a separate write-during-recovery proof burden without excluding repeated crashes. §4: Developer policy stops feature work when verification exceeds 20 seconds, then controls definition visibility, opacity/reveal and solver instantiation profiling. The discipline reduces search burden but cannot decide arbitrary verification, distinguish all timeouts from defects, or guarantee a fixed bound. Measured final passing definitions are not a distribution of failed proof attempts or controlled developer productivity. §5.1: linear means non-aliased mutable values and shared means temporarily borrowed aliased immutable values. Static checking forbids duplication and silent discard and restricts shared values to borrow scope; explicit free is allowed. Functional sequence semantics permit in-place C++ mutation without SMT heap-aliasing reasoning. Ordinary heap references still use dynamic frames, and can be held inside linear structures. §5.1 Figure 2: Trusted BoxedLinear<A> embeds a linear value in a freely aliased heap object. Take requires Has() and sets it false; Give requires no stored value. Borrow is restricted to pure functional callers so an imperative method cannot remove ownership during the borrow. SMT proofs establish Has() where ownership is not syntactically obvious. Thus the method combines type safety with proof obligations rather than enforcing all aliasing rules in a simple Rust-like typechecker. §5.2: Backend maps immutable datatypes to structs, heap arrays/classes to reference-counted objects and immutable sequences to shared storage plus offset/length. Linear sequences use in-place operations and explicit deallocation without reference counts. Mathematical integer executable code is rejected; refined machine integers must fit C++ types. Compiler and runtime correctness are trusted. §§6.1.1–6.1.2: Uses 2 MiB nodes on HDD, 128 KiB on SSD, fanout 8. Serialized lower nodes avoid conversion, while the root uses a mutable search tree for single insertions. A ghost per-index lseq_has sequence permits taking disjoint subsets of linear children during splits. Claims about Rust needing unsafe/Option are the paper authors’ comparison, not a general impossibility theorem about all safe Rust implementations. §6.1.3: LRU BlockCache tracks inter-block references and garbage collection. Persistent/frozen/ephemeral copy-on-write trees represent last completed checkpoint, checkpoint in flight and live updates. Logical-to-physical indirection uses linear-probing hash table; example 1 TiB disk requires 24 MiB table. Two alternating counter-tagged superblocks select the latest checkpoint. Correctness depends on modeled write completion and checksum semantics. §§6.1.3–6.1.4: Checkpoint writes dirty nodes, then indirection table, then a superblock. At checkpoint start dirty shared nodes become write-back-before-editing, preserving the frozen snapshot. A node write must be issued before modification but need not complete before modification; crash can recover the old checkpoint. Logical journal records each insertion; sync persists journal instead of repeatedly writing large nodes. Checkpoint reclaims journal space. §7.1: Table 1 implementation proof/executable ratio is about 4:1; including refinement proofs gives 7:1. These annotation counts are a proxy for final proof burden, not person-time, maintenance cost or specification adequacy. Authors observed no runtime correctness/data-loss bugs but did observe liveness/performance bugs; no duration or exposure denominator establishes a general failure rate. §7.1: Hash-table proof LOC 1678→1063 (about 37% lower), search-tree 2220→1531 (about 31% lower), with search-tree executable LOC increasing 289→373. This compares two author implementations and supports reduced annotation burden for those components, not a universal productivity effect. RocksDB test/production ratio 0.99 and BerkeleyDB 0.45 are not directly comparable correctness guarantees. §7.1 Figures 4–5: 98.3% final proof units under 10 seconds, 99.0% under 20; 37 exceed 20 seconds and 54% of those involve dynamic frames. Hide 308 definitions (18%), reveal 1403 times; 52 never revealed and 74% revealed at most five times. Visibility counts both overestimate and underestimate manual effort. Whole verification takes 1.8 CPU-hours, 11 minutes on 32 cloud machines, not 32 CPU cores in one machine. §7.1 reader qualification: Printed sentence says maximum verification time dropped 10s to 32s and 99th percentile dropped 1.3s to 4.8s. The endpoints increase in that order and conflict with dropped; the PDF visibly contains this wording. Do not silently reverse endpoints or claim a quantified speedup from this sentence without correction from source authors. §7.2: HDD/subcomponent runs use AWS d2.xlarge with four hardware hyperthreads, 2.4 GHz Xeon E5-2676 v3; SSD i2.xlarge has four hyperthreads, 2.5 GHz E5-2670 v2 and SATA SSD. All YCSB systems limited to one core and 2 GiB RAM; load 10 million operations/about 5 GiB, run phases 10000 operations. Reported medians and min/max over six runs, not confidence intervals. §7.2.1 Figure 6 reader calculation: Printed HDD Load medians are BerkeleyDB 233, VeriBetrKV-DF 5649, VeriBetrKV 5579 and RocksDB 44670 ops/s. Ratios from linear VeriBetrKV are about 23.9× faster than BerkeleyDB and 8.0× slower than RocksDB, matching abstract 24×/8× but not body/caption over 25× or caption about 9×. Preserve numerical evidence rather than reconcile by guessing different runs. §7.2.1: VeriBetrKV is slower than both other stores on most queries and roughly 4× below RocksDB, but HDD uniform U has RocksDB 35 versus VeriBetrKV 57 ops/s. SSD Load has VeriBetrKV 8986 versus BerkeleyDB 6664 and RocksDB 72645, about 1.35× faster/8.1× slower; body says 4× slower on SSD, inconsistent with printed load values. Workload-specific outcomes matter more than a universal performance claim. §7.2.1: Authors attribute slowdown to effective-cache reduction from fragmentation/conservative cgroup allocation, lack of overlap between CPU and flush I/O, and 1.5× more I/O than RocksDB, about half extra from checkpoint policy. Simulated 1.8 GiB cache exceeds 13K HDD insertions/s and matches 300K I/Os for 1M queries. These simulations/profiling attributions are not a measured optimized implementation. Query I/O usually 1.5 MiB versus RocksDB 4–8 KiB; future partial-node marshaling is unimplemented. §7.2.2: Microbenchmarks compare dynamic frames/linear on 64M random 64-bit-key hash operations and 8M search-tree pairs. Linear hash inserts and queries are faster but deletes slower; search inserts slower and queries faster. Authors suspect reference-count and reconstruction overheads; no isolated causal experiment is supplied. Dafny type extension is 1900 LOC (3%) and C++ backend 3100 (7.5%). Appendix A: Artifact Docker images include source, modified compiler, verification/performance scripts and graph generation. Any x86/x64 CPU with HDD/SSD, 20 GiB disk and several hours expected; source YCSB/config included. External proof bodies, compiler changes, durability implementation and benchmark scripts were not audited or replayed by this reader. No LLM-agent evaluation is present. - how much was read: most of it read - source; notes: Storage Systems are Distributed Systems (So Verify Them That Way!) - record id: `veribetrkv-2020` - EAST-ADL to UPPAAL verification (2019) - title: A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL - what: Defines formal EAST-ADL behavioral semantics and model-to-model rules that transform AnalysisFunctions, ports, triggers and behavioral constraints into UPPAAL timed automata, then model-checks safety, timing, deadlock and liveness requirements. The verification criterion restricts the source to functions, ports/connectors, artifacts and Behavioral Annex constraints; each AnalysisFunction becomes a timed automaton with atomic urgent READ/WRITE port actions. The transformation uses broadcast channels and global/local variables, with explicit rules for periodic time-triggering, event-triggering and bounded end-to-end response via an observer automaton. A six-function Volvo steering-system-unit (SSU) model is translated directly from Papyrus EAST-ADL without SAVE-CCM; UPPAAL checks deadlock freedom, leads-to/data correspondence, state exclusion, local execution bounds and observer-based bounded liveness. - number: 25 SSU properties were verified successfully - number: UPPAAL took around 2 seconds per property on an Intel T9600 2.80 GHz processor - number: Maximum explored state space was 38,166 states - number: Periodic execution-time bound example uses 0 ≤ clk ≤ 2 - limits: The method targets the Analysis level and assumes a FunctionalAnalysisArchitecture, broadcast communication, run-to-completion non-blocking functions and overwritable port buffers. The SSU case assumes a perfect one-time-unit periodic clock and mutually unsynchronized periodic functions; only three of six automata are shown due to space. Results are model-checking results for one industrial case, and future work explicitly leaves schedulability, resource properties and cross-level refinement for later. - how much was read: most of it read - - record id: `east-adl-to-uppaal-verification-2019` - Generating Verified LLVM from Isabelle/HOL (2019) - what: Isabelle-LLVM shallowly embeds a structured subset of LLVM in Isabelle/HOL, generates LLVM text, supplies a total-correctness separation logic and kernel-checked verification-condition generator, and retargets Sepref to synthesize imperative programs with explicit memory deallocation. Binary search and KMP refine mathematical specifications to fixed-width arrays/words. Details the executable state-error monad and structured memory semantics, proof-producing normalization to monomorphic instructions/recursive equations, separation ownership including allocation-size tags, framed total-correctness triples, and synthesis rules that insert deallocators when variables leave scope. Connects abstract algorithm proofs to overflow-safe64bit implementations while explicitly identifying the unverified text translation and ABI/runtime boundary. - limits: Total correctness is established for the shallow Isabelle-LLVM semantics through successful SUCC results, excluding FAIL and NTERM under the proved preconditions. Translation from shallow logical constants to actual LLVM text remains trusted; no proved correspondence to a deep LLVM semantics, optimizer, assembler, physical machine or OS is supplied. Memory is a finite list of allocation blocks with an unbounded supply of new blocks with structured pairs, pointers and fixed-width integers, rather than byte-level target memory. Pointer addresses have no finite bit width in the model. Floating point, poison values and structures beyond nested pairs are outside the supported fragment. Generated allocation calls use C calloc/free with architecture-dependent size_t; generator refuses potentially lossy size downcasts. Allocation-failure code exits1 after an error. Thus the claimed actual-program behavior permits out-of-memory termination rather than guaranteeing the modeled successful result under all finite resources. Recursive calls implicitly have unbounded stack in the semantics. Stack probing/split-stack protection is future work; likely guard-page termination is an informal engineering argument, not a proved resource bound or implemented universal protection. Application binary interface and correct C header are user responsibilities; C/LLVM ABIs only partially match. Correct callers, library behavior and target configuration therefore matter beyond proved Hoare triples. Refinement assertions impose representability and arithmetic bounds. Binary search requires sorted list, valid array/length representation and signed64bit elements; KMP requires |s|+|t|<2^63 and its arrays/word representations. Correctness is relative to these formal specifications, not arbitrary external input encodings. Kernel-checked preprocessing/VCG/Sepref proofs rely on Isabelle inference kernel and modeled logic. Incomplete preprocessing can fail or produce rejected shapes without supplying an unchecked proof. Trusted shallow semantics/text generation remains separate from these checked transformations. Only medium-complexity binary search/KMP case studies are demonstrated. Existing Imperative HOL basic data structures cannot simply be reused because of words/pairs; nested imperative containers currently need ad-hoc separation proofs. Large model-checker/SAT-solver ports and general overflow-refinement automation are future work. - how much was read: most of it read - source - record id: `generating-verified-llvm-from-2019` - LoFAT and HiFAT (2019) - title: Binary-Compatible Verification of Filesystems with ACL2 - what: Builds executable FAT32 model LoFAT and directory-tree specification HiFAT, proves their transformations/refinement in ACL2, and tests correspondence with existing Linux FAT32 and mtools implementations through disk-image co-simulation. HiFAT contains directory entries and complete file strings; LoFAT uses a single-threaded object close to the on-disk FAT32 layout. §4 proves termination, inverse transformations modulo equivalence, correct error behavior, and composition of image/LoFAT/HiFAT transformations. Clusterchain recursion is bounded by maximum file length; directory traversal uses a bound on total directory entries derivable from the data region, rather than an arbitrary nesting-depth limit. EqFAT ignores file order, allocation choices, deleted and dot entries, redundant FAT copies and metadata that does not remove data. Most POSIX operations execute by converting to HiFAT, operating there and converting back; equivalence justifies eliding repeated conversions. Direct open/pread/lstat versions are proved equivalent. Guard verification, stobjs, string representations and mbe proofs support efficient execution. Proofs found incorrect FAT bounds and an off-by-one directory attribute bug; Linux co-simulation exposed a missing one-cluster directory constraint and also found an ACL2 I/O bug. - number: 24,905 lines models/proofs; 619 lines co-simulation; 31 tests - number: 128MB image: 2.48s read, 4.14s write - number: 256MB: 3.58s read, 7.91s write; 512MB: 7.52s read, 15.46s write - number: 1024MB: 15.92s read, 24.87s write - limits: The theorem is refinement of the authors’ FAT32 model/specification; Linux and mtools correspondence is finite co-simulation evidence. LoFAT validity uses a deliberately minimal subset of the official FAT32 constraints. HiFAT excludes duplicate entries and imposes FAT32 size limits; malformed images/LoFAT states share an equivalence class. EqFAT sets aside creation/access/write times and long filenames, restricting claims about programs such as Make. statfs exposes metadata that EqFAT abstracts, limiting its co-simulation use. Multiple-process interaction, concurrency, crash consistency, hard links and generalization to ext4 remain future work. ACL2 OS I/O specification and implementation remain trusted/unverified interfaces; one discovered I/O bug illustrates this boundary. - how much was read: most of it read - - record id: `lofat-and-hifat-2019` - runtime certification of consensus (2019) - title: Certifying Safety when Implementing Consensus - what: Designs distributed certification agents that repeatedly check agreement and validity predicates supplied by a running consensus implementation. Agreement compares each local decision with child decisions on a certified spanning tree. Validity combines Boolean certificates that a local proposal equals the agreed value, and depends on concurrent agreement checking. Tree certification checks root consistency, acyclic distances, and an aggregate node count. Unique IDs are checked by comparing the multiset of IDs with their ordered successors using polynomial evaluation at n+1 points; this initialization is more expensive than normal certification. After failures the tree is rebuilt and soundness/completeness are weakened to inputs from non-faulty nodes. These are runtime checks of existing code rather than proofs of its implementation. - number: one combined agreement/validity message per node per check - number: O(n log n) bits per node for deterministic unique-ID initialization - number: n−1 fail-stop failures with properties restricted to non-faulty-visible inputs - number: up to O(n) communication rounds from tree height - limits: Nodes communicate over a partially synchronous network; certification agents share fate with implementation processes and only see local implementation inputs, not internal protocol messages. Failures are fail-stop, not Byzantine, because the implementation is assumed buggy but non-malicious. At least one agent must signal a violation, and operators must monitor agents. General predicates, automatic certificate synthesis, and automatic recovery after errors remain future work. IDs must remain stable across failures; variable-length decisions use cryptographic hashing and then have probabilistic soundness. Tree height can require O(n) communication rounds. - how much was read: most of it read - - record id: `runtime-certification-of-consensus-2019` - Dinv (2018) - title: Inferring and Asserting Distributed System Invariants - what: It mines likely invariants over distributed snapshots of Go programs, using static slicing, vector clocks and Daikon. It turns chosen invariants into runtime assertions. - number: four Go systems, 1.7K-144K lines - number: Serf: about 1 million invariants reduced to 40 by manual refinement - number: Raft assertions 11, 13, 72 lines; detection 0.07, 0.36, 2.22 s - number: always-on check 52x slowdown, 1% sampling 1.02x - limits: The invariants are likely, not verified. It is designed for runs where no node fails. Humans choose which properties matter and write the assertion functions. - how much was read: most of it read - source; notes: Related-work omission: Inferring and Asserting Distributed System Inva; notes: Related-work omission: Inferring and Asserting Distributed System Inva - record id: `dinv-2018` - DiVM: Model Checking with LLVM and Graph Memory (2017) - what: Presents DiVM, an LLVM-IR virtual machine with graph-organized memory and verification hypercalls, plus DiOS, a verification-oriented OS that supports POSIX-like C/C++ programs in explicit-state and abstraction-driven model checking. The VM represents heap objects as graph nodes linked by pointer edges, tracks pointer/definedness types in shadow memory, uses object-level allocation/free and stable object identifiers, and stores stacks as graph-linked activation frames. A small hypercall interface exposes nondeterministic choice, interrupt points, tracing, shared-object marking and machine control to a virtualized OS. This separation lets the verifier keep a simple initial/successor interface while the OS implements scheduling, threads, syscalls, monitors and faults. The paper explains τ and symmetry reductions, abstraction compatibility, and evaluates DIVINE 4 against DIVINE 3 and ESBMC. - number: DIVINE 4 runs 926 error-free models (from 1,045 total: 926 correct and 119 erroneous) in 8:15:44 and explores 33.0 million states. - number: Compared with DIVINE 3 on 457 models, DIVINE 4 takes 1:05:17 versus 7:00:33 and explores 4.729 million versus 11.6 million states. - number: Against modified DIVINE 3 on 448 models, DIVINE 4 takes 29:27 versus 5:01:40 and explores 1.820 million versus 5.803 million states. - number: ESBMC comparison covers 60 models: DIVINE 4 takes 10:22 versus ESBMC 2:43:39. - limits: The target is mainly C/C++ units with no uncontrolled external input; scheduling and failures are nondeterministic, while malloc/new are assumed non-failing for most benchmarks. Runtime typing is required because LLVM memory is untyped and casts defeat static recovery. Pointer-to-number conversions can invalidate heap canonicalization, so noncanonical state forms must be retained for successor generation. IPC/shared-memory pointers need OS translation to preserve isolation. Evaluation is explicit-state and depends on DiOS/library coverage; comparisons expose DIVINE 3 omissions and ESBMC's limited C++ support. - how much was read: most of it read - - record id: `divm-model-checking-with-2017` - Ivy repository (2016) - title: Ivy: Safety Verification by Interactive Generalization - what: Ivy is a research tool for interactive development of protocols and correctness proofs, with interactive visualization of automated proofs and a human/tool workflow for exposing errors. - number: Bounded verification about 10 transitions in a few minutes - number: Pages 614-630 - limits: README is brief and points to the website for details. - how much was read: most of it read - source; notes: tools - record id: `ivy-repository-2016` - PrDK protocol programming with automata (2016) - what: Presents PrDK, an Eclipse development kit separating sequential process code from automata-based protocol code, with graphical Reo and textual Pr syntax, automata composition/interpreting, and Java compilation. The paper explains port put/get blocking semantics and automaton transitions as admissible data flows; composition from primitive automata avoids direct state-machine authoring. Reo-to-Pr enables parameterized protocols, while parser/interpreter/compiler stages generate a Java protocol class whose monitor thread completes pending operations. Bisimulation-preserving automata optimizations improve generated code. - number: 7 NAS benchmarks - number: 126 tests - number: 2, 4, 8, 16, 32, 64 processes - number: 37% within 10% slower; 38% faster - limits: Implemented target is Java and assumes multithreading, synchronous port operations, and finite automata products. Product size can affect scalability. The paper evaluates execution but does not include prior Reo model checking; seamless verification integration is future work. Reo lacks generic parametrization, requiring Pr for k-process variants. - how much was read: most of it read - - record id: `prdk-protocol-programming-with-automata-2016` - A Messy State of the Union: Taming the Composite State Machines of TLS (2015) - what: The authors test TLS libraries for state-machine bugs by generating traces that deviate from the allowed behavior. They also write a replacement C state machine for OpenSSL and prove in Frama-C that it only allows traces from a hand-written list of allowed traces. A Coq proof shows that two sides with equal handshake logs are in equal states. - number: 8 libraries tested, flaws in 6, ten attacks including eight impersonation attacks - number: replacement about 750 C lines; invariant spec about 460 lines; annotations about 900 lines - number: about 2 minutes per function, 30 minutes total - number: Eight libraries tested, serious flaws in six, ten attacks including eight impersonation attacks - limits: The work proves nothing about integrity or confidentiality. It does not prove that the system eventually makes progress. It covers one component, not the whole library. The human effort was not timed. The authors read the 2015 version, not the CACM version. - how much was read: most of it read - source; notes: A Messy State of the Union: manual specification and annotations, auto; notes: A Messy State of the Union: manual specification and annotations, auto - record id: `a-messy-state-of-2015` - IronFleet (2015) - title: IronFleet: Proving Practical Distributed Systems Correct - what: It proves a replicated state machine (IronRSL) and a sharded key-value store (IronKV) correct, down to Dafny code. The liveness proofs are built by chaining intermediate progress conditions. - number: 1,400 specification, 5,114 implementation, 39,253 proof lines; 395 minutes to check - number: IronRSL liveness: 7,869 proof lines, 115 minutes; IronKV liveness: 2,093 lines, 23 minutes - number: about 3.7 person-years - number: implementation-level proof/code ratio 3.6 - limits: The top-level spec, event loop, Dafny, runtime, OS and hardware are trusted. IronRSL liveness needs eventual timing bounds and a live quorum. The reduction argument is on paper. - how much was read: most of it read - source; notes: S8 - record id: `ironfleet-2015` - Verdi (2015) - title: Verdi: A Framework for Implementing and Formally Verifying Distributed Systems - what: Verdi proves an application correct under an easy network model. Then a verified system transformer changes the implementation so that it tolerates a harder fault model, and carries the property over. The proofs are in Coq. - number: Table 2 (spec / implementation / proof LOC): KV 41/138/337; primary-backup 20/134/1155; composition 5/N/A/19; Raft linearizability 170/520/4144 - number: Table 2 lines spec/impl/proof: sequence numbering 20/89/576; KV 41/138/337; primary/backup 20/134/1,155; Raft linearizability 170/520/4,144 - number: no comparable total person-time established in the review - limits: The network semantics and the TCB (the trusted computing base) are in Section 3. This paper is not the later complete Raft linearizability result. - how much was read: most of it read - source; notes: S29; notes: Choosing top-level distributed guarantees and trusted boundaries; notes: Appendix B: Concrete systems and theorem scope - record id: `verdi-2015` - ASM2Bogor (2014) - title: An Efficient Solution for Model Checking Abstract State Machine Using Bogor - what: Presents ASM2Bogor, an automatic translator from AsmetaL abstract-state-machine specifications to Bogor's BIR language, including domains, functions, initialization, transition rules, monitored inputs, parallel/forall rules, LTL properties and invariants, followed by model checking and counterexample generation. The report defines validation for unsupported constructs (for example forall over infinite Integer domains), maps abstract/enumerated/subset/sequence domains and controlled/derived/monitored functions, encodes parallel rules using invisible guarded BIR locations and changed-variable tracking, and rewrites AsmetaL LTL/invariants into Bogor temporal-property functions. Six case studies exercise sluice-gate, one-way traffic-light, dining-philosophers, critical-section, tic-tac-toe and ferryman models. - number: 6 case studies - number: tic-tac-toe 596638 transitions/49304 states - number: dining philosophers 8801 transitions/353 states - number: sluice gate 1041 transitions/81 states - limits: Only AsmetaL constructs with a BIR mapping are accepted; infinite-domain forall is rejected, and monitored functions are represented by nondeterministic threads because environment interaction is unavailable. State-space exploration inherits Bogor's finite-state/model-checking limits. The ferryman case exposes a false property and one error, showing modeling/specification mistakes are detectable rather than proving all models correct. - how much was read: most of it read - - record id: `asm2bogor-2014` - Model-Based Trace-Checking (2011) - what: Replays observed traces of a distributed Java travel-booking application through B (ProB) and Promela (Spin) models. It checks invariants and a resource-allocation progress property on those particular traces. - number: six invariant clauses - number: progress bug: keeps trying Hotel1 when it is full but Hotel2 has a room - limits: It finds errors but cannot show there are none. The match between model and code is assumed from inspection. Tracing code was inserted by hand. No success rate, size or time is given. - how much was read: most of it read - source; notes: Model-Based Trace-Checking - record id: `model-based-trace-checking-2011` - SLCO ASF+SDF Semantics (2011) - title: Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models - what: An executable prototype translates SLCO models of communicating objects into configuration-and-step models, then labeled transition systems, then Dot and existing verification-tool formats. Its worked verification is manual graph inspection following a reported mCRL2 reduction; a formal operational semantics and timing analysis remain future work. The paper spells out the intermediate CS language and selected ASF+SDF rewrite rules, including the non-atomic splitting of SLCO transitions, and uses a running lossy-channel example to show translation, visualization, hiding, and branching-bisimilarity reduction. The benefit argued is reuse of LTS tools and efficient term sharing, not a proved semantics-preserving compiler or a measured performance improvement. - number: One running two-object communication example, seven figures, nine printed listings; no benchmark suite, runtime, memory measurements, or correctness proof of the translator - number: ltsconvert is reported as used to hide labels and reduce the example by branching bisimilarity; the stated property is then judged by manual graph inspection (§4.2, printed p.77) - number: CADP BCG/AUT and mCRL2 checks are described as available routes; no supplied temporal formula, checker transcript, or additional verified case establishes that these routes were exercised for a specific property - number: Syntax safety and memory/execution efficiency are attributed to ASF+SDF and ATerms; these are qualitative technology claims without measurements here - limits: State-space generation repeatedly explores reachable configurations until none is new, so a finite reachable space and adequate resources are needed for termination in practice. Variables include unbounded-looking integers and channels have buffers; no general finite bound is established here. The relation between prototype rules and an independent formal SLCO semantics is not proved. Time-delay analysis is future work. The “exactly two” reception property is stated by inspection after abstraction, without a temporal formula or fairness assumption; infinite lossy behavior must not be silently turned into eventual-delivery liveness. - how much was read: most of it read - source - record id: `slco-asf-sdf-semantics-2011` - uc-klee equivalence cross-checking (2011) - title: Practical, Low-Effort Equivalence Verification of Real Code - what: Presents uc-klee, which automatically gives two C functions symbolic inputs, lazily creates pointed-to data and cross-checks outputs/errors on explored paths; evaluates libc implementations, revisions, compiler optimizations and self-checks. §2 describes an automatic harness that snapshots memory, executes one function, restores original values while retaining constraints, executes the other, then compares escaping results or error type. User wrappers filter invalid inputs or canonicalize allowed output differences, exemplified by isdigit. §3 tracks referents in symbolic shadow memory so low-level pointer/integer casts and symbolic-index accesses work. Output comparison recursively follows return/argument-reachable memory, comparing data and pointer offsets while allowing allocation addresses to differ; unrelated globals are omitted. Lazy initialization handles unbound pointers through unique symbolic objects, constrained addresses, size-doubling from 8 bytes and nested-allocation depth limits. §4 distinguishes instruction coverage from path exhaustion and uses identical-code cross-checking to expose verifier nondeterminism and pointer-tracking defects. Comparing O0/O3 versions exposes a confirmed LLVM 2.6 memmem optimizer defect. - number: cross-library 143 checked: 66 verified, 57 different, 15 timeouts, 4 KLEE-limited, 1 uc-klee-limited; at least 7 actual bugs - number: revision comparison 203 checked: 84 verified, 20 different, 30 timeouts, 56 KLEE-limited, 13 uc-klee-limited; 2 new bugs and 5 patched bugs - number: optimizer comparison 622 checked: 335 verified, 70 differences, at least 1 confirmed LLVM defect - number: self-check 622 checked: 335 verified, 12 differences; median coverage 100% - limits: Equivalence holds only for the finite explored paths, bounded object sizes/depth, single invocation in isolation, chosen compiler and architecture. If both functions make the same mistake, cross-checking cannot detect it; matching error types count as equivalent even with different root causes. Lazily allocated objects cannot alias existing objects, missing overlap/circular-buffer behaviors; some address constraints cannot be realized. Unbound function pointers are unsupported. KLEE concretizes symbolic allocation sizes and floating-point operands, potentially missing other values; unresolved externals, symbolic external-call arguments, inline assembly and structure returns can make paths unverifiable. Global state is compared only when reachable through returned/formal-argument pointers. Reference behavior and filtering wrappers replace a formal intended-behavior specification, and differences are not automatically bugs. - how much was read: most of it read - - record id: `uc-klee-equivalence-cross-checking-2011` - D3S (2008) - title: D3S: Debugging Deployed Distributed Systems - what: Developers write C++ predicates over consistent global snapshots. D3S injects instrumentation into running programs and checks the predicates. It reports the state histories that violate them. - number: 5 deployed systems, results within one month - number: PacificA 67,263 code lines / 118 predicate lines, 3 bugs; MPS Paxos 6,993 / 50, 2 bugs - number: runtime overhead less than 8%, below 2% in search and BitTorrent cases - number: 5 deployed systems, PacificA 67,263 code lines / 118 predicate lines with 3 correctness bugs; MPS Paxos 6,993 / 50 with 2 bugs - limits: It checks observed runs and does not prove anything. Snapshot correctness depends on group membership. The window is finite, so it cannot check liveness over infinite runs. Developers must pick useful predicates. - how much was read: most of it read - source; notes: D3S: Debugging Deployed Distributed Systems; notes: D3S: Debugging Deployed Distributed Systems - record id: `d3s-2008` - Tale of Two Clocks (1996) - title: Refinement in State-Based Formalisms - what: A seven-page note that uses a clock to explain hidden state, stuttering internal steps (steps that change nothing visible), and refinement. - limits: It is a teaching note. It has no runnable artifact. - how much was read: most of it read - source; notes: connecting different descriptions of the same behavior - record id: `tale-of-two-clocks-1996` - Anvil repository - title: Anvil: Building Formally Verified Kubernetes Controllers - what: Anvil implements Kubernetes controllers in Rust, specifies their properties in Verus-TLA, and proves an Eventually Stable Reconciliation property. Its Welder extension composes liveness proofs across controllers. - number: Three built-in controllers (ReplicaSet, Deployment, StatefulSet) and one RabbitMQ controller are reported in the README. - limits: The README says verification still requires SMT theorem-proving expertise; examples and assumptions are repository-specific. - how much was read: most of it read - source - record id: `anvil-repository` - Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification - what: Develops a workflow translating Message Sequence Chart bus-protocol specifications into SMV verification programs, with syntax/semantic analysis intended to detect deadlocks and protocol inconsistencies before implementation. - number: Formal verification uses the SMV model checker - number: No substantial runtime or benchmark suite reported - limits: The approach relies on MSC expressiveness and a translation preserving the modeled protocol; verification is bounded by the generated SMV model and selected bus scenarios. The report presents methodology and examples rather than broad quantitative benchmarking. - how much was read: most of it read - - record id: `bus-protocols-msc-based` - Disel repository - title: Disel: Distributed Separation Logic - what: Disel is a Coq framework for implementing and compositionally verifying distributed systems and clients. Its embedded DSL separates protocol specifications from implementation details. - limits: README-level documentation; no new paper claims are added. - how much was read: most of it read - source - record id: `disel-repository` - Perennial repository - title: Perennial - what: Perennial verifies Go programs in Lean 4 on top of iris-lean. The README prescribes one specification and proof file per Go function and documents a bounded layer with explicit time and thread receipts. - limits: The current Lean branch says it does not cover crash/recovery reasoning; bounds are parameters and proofs must carry bound premises. - how much was read: most of it read - source - record id: `perennial-repository` - Verdi repository - title: Verdi - what: Verdi is a Coq framework for implementing and verifying distributed systems across fault models. Verified system transformers let a proof in an idealized model transfer to an analogous adversarial environment. - limits: The README points to related Raft papers; this record is repository documentation, not a new paper reading. - how much was read: most of it read - source - record id: `verdi-repository` - Verified IronKV - title: Verified IronKV (IronSHT port) - what: This repository ports IronFleet’s IronSHT host program to Verus. Its README explicitly says it verifies implementation-level reasoning but does not reproduce IronFleet’s proof that the host program implements the distributed TLA state machine and high-level specification. - limits: The repository omits IronFleet’s distributed refinement layer, so it is not a complete end-to-end proof. - how much was read: most of it read - source; notes: D3 - record id: `verified-ironkv` - Closing the verification loop (harness-first agents) (2026) - what: Datadog describes agents that build systems under a harness (test setup) that a human defines. The human defines the system idea and invariants, and reviews the simulation harness. - number: Mental overhead roughly 2-3x the effort of writing the code itself - limits: A vendor post, not peer reviewed. - how much was read: parts read - source - record id: `closing-the-verification-loop-2026` - Corten (2026) - title: Corten - Foundational Verification of Rust Programs - what: A framework in the Rocq proof assistant for proving Rust programs correct with separation logic (a logic for reasoning about who owns which memory). It defines Rust's behavior on the compiler's typed high-level IR so proof goals look like Rust source, and adds tactics that follow the code's shape. - number: Automated proofs are about 2x to 4x shorter than proofs done directly against the semantics, on a synthetic test suite - number: Buddy allocator case study: about 300 lines of Rust, about 2800 lines of Rocq (about 250 spec, about 800 general Rust reasoning, about 1400 free-list lemmas) - number: Specifications about 2x the size of the code; automated proofs 2x to 4x the Rust size - limits: Soundness of the semantic axioms is proved only for the pure and heap-statement fragments so far; the rest is itemized in an appendix. Specs of Rust core functions used by the case study are not proved. Single-threaded in practice (concurrency inherited from Iris but not yet exercised), traits only partly handled, no labeled break/continue. Allocator spec covers memory safety, not allocation quality. - how much was read: parts read - source; notes: Corten (2026) - record id: `corten-2026` - Lion (2026) - title: Lion: Modular Verification of Async Runtime Liveness - what: Lion is a Tokio-like async runtime written in Rust and verified in Verus. Its top theorem says that, under stated assumptions, a spawned task is eventually polled to completion. The liveness claim does not use temporal operators. Instead it is a bound on how long a task waits, under a filter on what the environment may do. - number: 3,393 lines executable, 39,648 lines spec/proof, 507 trusted (about 11.7 to 1) - number: 126 external_body items in the trusted base - number: Full verification run takes a few minutes - number: At least 95% of unverified-runtime throughput on nine workloads (claim) - limits: No machine-checked proof shows that the compiled runtime matches the model. The SOSP paper is not public, so the notes read the tech report and the repo in part. - how much was read: parts read - source; notes: Lion: Modular Verification of Async Runtime Liveness; notes: Newly found 2026 Verus liveness: Lion - record id: `lion-2026` - OmniLink (2026) - what: OmniLink validates traces of unmodified concurrent code. It treats each operation as a black box with a time window and a TLA+ meaning. - number: Two previously unknown bugs (BAT, ConcurrentQueue) - limits: It was only tested. Distributed systems are left as future work. - how much was read: parts read - source - record id: `omnilink-2026` - Quint Connect (2026) - title: Quint Connect / tla-connect - what: A model-based testing framework for Rust. A driver maps Rust state to model state, executes generated Quint traces, and compares states. - limits: The driver is an explicit link that a human or agent writes. A pass shows agreement on the tested traces only. A wrong projection of state can hide a bug. - how much was read: parts read - source; notes: R06. Quint Connect, Choreo, and LLM-driven implementation - record id: `quint-connect-2026` - Tulip (2026) - title: Verifying a high-performance distributed transaction system using permissioned state machines - what: Tulip is a distributed transaction system. It comes with a machine-checked proof that the implementation meets a spec identical to that of a local transaction system that is strictly serializable. The method combines TLA-style protocol invariants (facts that stay true in every reachable state) with separation-logic permissions. - number: about 4,000 lines of Go, about 42,000 lines of Rocq (about 11x) - number: 10 module types - number: bugs caught: transactional read, lock release, TAPIR timestamp inversion - number: 3,956 lines of Go code (abstract) - limits: The spec does not capture liveness, and the authors did not explore whether the method applies to liveness. The PDF does not name the venue. - how much was read: parts read - source; notes: Verifying a high-performance distributed transaction system using perm - record id: `tulip-2026` - Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems (2026) - what: The paper writes four concurrency anomalies of shared memory between LLM agents in TLA+, checked with TLC. It verifies Rust detectors and runtimes in a Verus crate. - number: 274 Verus obligations (zero assume, zero admit) - number: 24 obligations for the spec-implementation chain; refinement obligations 31 (pessimistic), 18 (SSI projection) - number: 274 Verus proof obligations - limits: Nothing mechanical links the TLA+ and Verus parts. The TLAPS proofs only check that the texts agree, and the Verus refinements are against Verus state machines. It covers safety only, and the authors state that liveness is a gap. It has a single author and the results are self-reported. The notes read about 25% of the paper. - how much was read: parts read - source - record id: `verified-detection-and-prevention-2026` - 3SF model checking (2025) - title: Technical Report: Exploring Automatic Model-Checking of the Ethereum specification - what: The authors translate the Python spec of Ethereum's 3-slot-finality (3SF) consensus protocol into TLA+ and use the Apalache model checker to test Accountable Safety: if two conflicting chains are both finalized, at least one third of validators can be shown to have broken a voting rule. They then add hand-made abstractions and re-encode the problem in SMT (CVC5) and Alloy to check larger instances. - number: Direct translation (Spec2): checking Accountable Safety timed out after more than 40 hours (Table 1) - number: Alloy with Kissat: Accountable Safety holds for up to 6 blocks; e.g. 5 blocks, 25 checkpoints, 12 votes in 234 s (Table 5) - number: CVC5: verified up to 5 blocks with 5 checkpoints (1h 40m) or 3 blocks with 6 checkpoints (74h) (Table 4) - number: A 7-block Alloy run went over 16 days without finishing - limits: Only the finality gadget and only Accountable Safety, on small bounded instances (at most 7 checkpoints and 24 votes); every validator has stake 1. The hand-made abstractions are not proved equal to the Python spec. Appendix A (translation rules) and B (soundness proofs) were skimmed, not read closely. - how much was read: parts read - source; notes: ## Exploring Automatic Model-Checking of the Ethereum specification (2 - record id: `3sf-model-checking-2025` - A Refinement Methodology for Distributed Programs in Rust (precursor: Refinement Proofs in Rust Using Ghost Locks) (2025) - what: Proves that Rust distributed programs match a simpler model of what they should do (a refinement proof), using the Prusti verifier. The precursor paper also proves liveness (something good eventually happens). It writes those proofs as ghost code (code used only for proving, never run), using a direct encoding of LTL (a logic for statements about time). Cases include a simplified Memcached. - limits: The review notes could not get the final OOPSLA PDF and read the precursor instead. The verifier is Prusti, not Verus. The review notes do not know whether the final version keeps the liveness part. - how much was read: parts read - source - record id: `a-refinement-methodology-for-2025` - Anvil thesis (2025) - title: Building and Verifying Cloud Infrastructure Systems with State-Centric Reasoning (PhD dissertation) - what: The thesis proves liveness of Kubernetes controllers in Verus, using the Anvil framework. The human writes one general liveness formula, "eventually stable reconciliation": if the desired state stops changing, the cluster eventually matches it and stays that way. The proof splits into two parts: the environment becomes stable, and the controller reaches the desired state. - number: about two person-months to verify the ZooKeeper controller, about two person-weeks for each of the other two - number: each controller takes around 2.5 person-months to implement and verify; proof-to-code ratio 4.5 to 7.4 - number: ZooKeeper: executable 1,134 lines, proof 8,352 (ESR 7,245), trusted 950; RabbitMQ: executable 1,598, proof 7,228, trusted 548 - number: framework: 5353 lines of reusable lemmas, 7817 lines of trusted code; 70+ temporal-rule lemmas, 60 Kubernetes-environment lemmas - limits: The controller must be a state machine whose actions are atomic (they cannot be interrupted). The proof trusts the environment model, the shim layer, external APIs, the verifier, the compiler and the OS. After verification, testing still found one bug. It came from an incomplete spec of a trusted ZooKeeper API. About 40% of the 111 pages were read. - how much was read: parts read - source - record id: `anvil-thesis-2025` - Design and Modular Verification of Distributed Transactions in MongoDB (2025) - what: A TLA+ spec of MongoDB distributed transactions, with a modular spec of the interface. A follow-up blog generates conformance tests against WiredTiger. - number: TLA+ spec about 571 lines plus storage spec about 332 lines - number: 87,143 generated tests in about 40 minutes on a small finite model (2 keys, 2 transactions) - limits: It is tested only. Code is at https://github.com/mongodb-labs/vldb25-dist-txns. - how much was read: parts read - - record id: `design-and-modular-verification-2025` - EVMYulLean (2025) - what: A formal model of the EVM and Yul in Lean 4, with Ethereum conformance tests. It is used as the semantics underneath EqiVM. - limits: The README documents limits in its Yul semantics, including omitted gas and contract creation. No standalone paper was found. It is not an agent benchmark. - how much was read: parts read - source; notes: Bytecode-semantics prerequisites: repository evidence and retrieval ga; notes: Bytecode-semantics prerequisites: repository evidence and retrieval ga - record id: `evmyullean-2025` - gen-server-verification (2025) - what: This is the artifact of a master's thesis. A Java translation layer turns PlusCal into Erlang GenServer modules. Some modules are supplied by hand. The generated Erlang passed the OTP test suite and extra QuickCheck tests. - limits: The tests support usability and conformance. They do not prove that the generated Erlang refines the model. The author's name, institution and the thesis PDF were not established. - how much was read: parts read - source; notes: R04. Elixir generation and Erlang GenServer generation - record id: `gen-server-verification-2025` - ModelFuzz (2025) - title: Model-guided Fuzzing of Distributed Systems - what: ModelFuzz is a fuzzer. Its coverage goal is the number of states of an abstract TLA+ model that it reaches. It targets 2PC, etcd-raft and RedisRaft. - number: 12 previously unknown bugs (v3 abstract; the arXiv 2024 abstract in another note says 13), four only found by model-guided fuzzing - limits: It tests only. The two notes disagree on the bug count (12 vs 13). - how much was read: parts read - source - record id: `modelfuzz-2025` - Shipwright (2025) - title: Shipwright: Proving liveness of distributed systems with Byzantine participants - what: A Dafny framework. A node is written as event handlers and compiled to Go. A refinement proof shows that the real handlers, running over a network model that eventually stabilizes, give safety and liveness. The case study is PBFT agreeing on one log entry, with infinitely many views. - number: Shipwright 13,357 lines (1,351 trusted); PBFT implementation 31,138 lines (266 trusted) - number: total 1,617 trusted, 42,878 untrusted, 44,495 lines - number: proof found three liveness bugs (bad new-view signatures, wrong certificate counting, timer started too early) - number: implementation 1888 lines (Figure 11, PDF p.11) - limits: It assumes partial synchrony (the network eventually stabilizes), an unverified Go runtime, and unforgeable signatures. It covers only one PBFT iteration. Reply messages to clients are not in the top-level theorem. Some refinements are unfinished. Person-time is not given. - how much was read: parts read - source - record id: `shipwright-2025` - Terzian TLA+-to-Rust (2025) - title: A Tale of Two Refinements: LLM-assisted TLA+ to Rust - what: The report repeatedly refines TLA+ models and asks Gemini to implement an image-cache example as multithreaded Rust. Its history records a livelock (threads keep running but make no progress) and a premature termination. Both needed correction. - limits: This is a project report and is not peer reviewed. No Verus proof was found. The claim of "fully verified, spec-driven code generation" is only a possibility. - how much was read: parts read - source; notes: R01. A Tale of Two Refinements: LLM-assisted TLA+ to Rust - record id: `terzian-tla-to-rust-2025` - Vest (2025) - title: Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust - what: Users describe a binary format, and Vest generates Rust parsers and serializers verified in Verus. It uses a reusable combinator library. - number: about 6K library lines, verified in under ten seconds - number: DSL compiler 5,807 Rust lines - number: format descriptions: Bitcoin about 67 lines, TLS 1.3 about 500, WebAssembly about 600 - limits: It proves that parse and serialize are inverses, plus memory safety. It does not prove consensus or handshake security. Timing side channels are not a Verus theorem. The DSL frontend is unverified. - how much was read: parts read - source; notes: Vest: Verified, Secure, High-Performance Parsing and Serialization for - record id: `vest-2025` - ZENITH (2025) - title: ZENITH: Towards A Formally Verified Highly-Available Control Plane - what: A microservice SDN (software-defined networking) controller. Its TLA+/PlusCal spec is verified to ensure that the network state eventually matches the intent. Code is generated from the spec. - number: spec is 8.6K lines - number: eight properties P1-P8 proved by hand in TLAPS - number: 26 race conditions from prior SDN controller bugs (9 state inconsistencies, 7 deadlocks) - limits: The code generator is assumed correct, as with PGo. Model checking alone does not scale across topologies. TLAPS needed history variables (extra variables recording the past). Person effort is not given. - how much was read: parts read - - record id: `zenith-2025` - Fairneris (2024) - title: Fairneris: Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic - what: An AnerisLang implementation of Stenning transfer over UDP-like networking. Under fair scheduling and a fair network (nothing is delayed forever), every sequence number is eventually acknowledged. Coq checks the refinement (that the code matches the model) and most of the infrastructure. - limits: The model's liveness theorem is a pen-and-paper proof, not machine-checked. The review notes did not establish the venue, date or artifact. - how much was read: parts read - source; notes: papers and boundaries - record id: `fairneris-2024-2` - FizzBee (2024) - title: Fizzbee, Liveness and Fairness (tutorial) - what: These are tool docs for FizzBee's liveness syntax. 'Always eventually' means a good state recurs. 'Eventually always' means the system stabilises. Fairness is set per action: weak, strong, or unfair by default. - limits: The example is a toy. There is no CTL support. The notes cover about half of the docs. - how much was read: parts read - source; notes: FizzBee - record id: `fizzbee-2024` - Kondo (2024) - title: Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs - what: Kondo derives inductive invariants for Dafny protocol proofs from the protocol's structure. This reduces the invariants the user must write. - number: Paxos: 418 lines, Kondo needs 20 user invariants, 777 total proof lines, 42.9 s - number: IronFleet 4,581 lines of Dafny and Verdi 50,000 lines of Coq for manual proofs - number: Paxos row: 631 model lines; 27 invariant clauses without Kondo vs 20 synchronous; 856 proof lines without Kondo vs 557 synchronous plus 220 modified - number: Table 1 p. 848: 10 systems (Echo Server, Ring Leader Election, Simplified Leader Election, Two-Phase Commit, Paxos, Flexible Paxos, Distributed Lock, ShardedKV, ShardedKV-Batched, Lock Server) - limits: Liveness proofs are beyond its scope. Line counts are not measured human hours. - how much was read: parts read - source; notes: papers inspected - record id: `kondo-2024` - SandTable (2024) - title: SandTable: Scalable Distributed System Model Checking with Specification-Level State Exploration - what: It model-checks a TLA+ spec quickly, then replays the bug traces in the code. A conformance checker replays model traces to find places where the spec and code differ. - number: 23 bugs, 18 new, 17 confirmed, 13 fixed - number: Half a person day to a few person days to fix modeling errors; two person weeks adapting ZooKeeper specs - number: 114x-2989x faster state exploration - number: abstract: 18 new bugs, 17 confirmed, 13 fixed (the note's sentence adds 'out of 23 total' garbled) - limits: It cannot guarantee that no differences remain between the spec and the implementation. - how much was read: parts read - source; notes: P10. SandTable: Scalable Distributed System Model Checking with Specif - record id: `sandtable-2024` - Trillium / Fairis (2024) - title: Trillium and Fairis - what: A program-logic framework in Coq and Iris. Fairis proves liveness of concurrent programs under fair scheduling, by refinement of a model. The Aneris instantiation proves that distributed implementations refine TLA+ models (two-phase commit, single-decree Paxos and a CRDT). - number: about 1100 lines of proof scripts for Paxos - limits: The step from TLA+ to the Coq model was done manually. The distributed refinements give trace safety only. Distributed liveness is in a later manuscript. The notes' author read about 40%. - how much was read: parts read - source - record id: `trillium-fairis-2024` - Mocket (2023) - title: Model Checking Guided Testing for Distributed Systems (Mocket) - what: Mocket finds inconsistencies between a TLA+ spec and a distributed system's implementation. It annotates Java state and actions and exports TLC's state graph. It generates paths through the graph. It then drives implementation runs with instrumentation and a testing server. - limits: The notes could not find the publication's authors, venue or year. Coverage depends on the paths, the action mapping, the instrumentation and the configured faults. The notes found no universal theorem about the implementation or progress. - how much was read: parts read - source; notes: Mocket - record id: `mocket-2023` - PGo (2023) - title: Compiling distributed system models with PGo - what: It compiles Modular PlusCal models into Go. - number: Table 2 (MPCal SLOC; glue SLOC; effort): lock service 67; 87; 2 person-days; Raft 771; 676; 22 person-days; distributed KV 256; 383; 3 person-days; primary-backup KV 420; 270; 10 person-days; state-based CRDT 160; 185; 10 person-days - number: monolithic RaftKV: 25 person-days, 758 model lines, 1099 glue lines - limits: It gives no guarantee about the compiler. - how much was read: parts read - source; notes: P07. Compiling Distributed System Models with PGo; notes: papers - record id: `pgo-2023` - Proving Refinement in a Rust Verifier (MSc thesis) (2023) - what: A way to prove that a Rust program, checked by Prusti, refines a TLA+ model (every step of the program matches a step of the model). The model state is ghost state (proof-only state) behind a "ghost lock". Each implementation step takes the lock to perform one model step. - number: Paxos acceptor phases: 112 model / 132 implementation / 152 proof lines (3.5 min) - number: lock-free hash set: 123 / 57 / 376 lines (3 min) - limits: It covers safety only. Prusti lacks support for ghost code. The translation from TLA+ is manual and not implemented as automatic. The notes' author read about 35%. - how much was read: parts read - source - record id: `proving-refinement-in-a-2023` - Applying Formal Verification to Microkernel IPC at Meta (2022) - what: Meta proved two lock-free queues, used for message passing between processes in an OS under development, using Iris and Coq. The proofs cover verified pseudocode of the algorithm, not the C code. - number: Entire IPC implementation about three thousand lines - number: Six months with two engineers - limits: The specs say nothing about liveness (that operations eventually finish). A queue whose operations loop forever would satisfy them. - how much was read: parts read - source - record id: `applying-formal-verification-to-2022` - Sift (2022) - title: Sift: Using Refinement-guided Automation to Verify Complex Distributed Systems - what: Starting from a specification, an implementation model and intermediate layers, it turns each layer-to-layer obligation into a safety problem. It infers invariants with IC3PO and generates C++ with Ivy. - number: six cases: leader election, distributed lock, two-phase commit, sharded hash table, Raft, Multi-Paxos - number: manual work under five minutes for the three small cases, one person-month for Raft, three person-weeks for Multi-Paxos - number: Raft proof effort 1 person-month - number: MultiPaxos effort 3 person-weeks - limits: The top-level abstraction proofs for Raft and Multi-Paxos are manual or reused. Imperative optimizations may need loop invariants written by hand. It targets C++, not Rust. - how much was read: parts read - source; notes: papers inspected; notes: Sift: refinement from protocol down to executable systems - record id: `sift-2022` - ShardStore (2021) - title: Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 - what: Executable reference models and checks for the S3 ShardStore storage node. - number: Reference models about 1% of implementation code - number: Checks and harnesses 12% of the code base - number: Prevented 16 issues from reaching production - number: 18% of reference model and harness code written by the engineering team - limits: Passing the checks does not mean the code is correct. - how much was read: parts read - source; notes: papers; notes: Using Lightweight Formal Methods to Validate a Key-Value Storage Node - record id: `shardstore-2021` - eXtreme Modelling (2020) - title: eXtreme Modelling in Practice - what: MongoDB compared two ways to link a model to code. One is model-based trace checking (MBTC), which checks whether logged runs fit the model. The other is model-based test-case generation (MBTCG). Trace checking of replication was impractical. For Realm Sync's operational-transformation rules, a Go generator turned TLC states into C++ tests. - number: Realm Sync table (§5.2): 795 TLA+ lines, 755 Go lines, 4 weeks total effort - number: Abandoned trace checking after 10 weeks - number: 4913 generated tests reached 100% branch coverage vs 21% handwritten and 92% AFL fuzzer - limits: Trace checking of replication struggled with the level of abstraction, concurrency, incomplete observations, and keeping code and model in sync. The generated tests cover local merge behavior, not the whole distributed product. - how much was read: parts read - source; notes: P04. eXtreme Modelling in Practice - record id: `extreme-modelling-2020` - Pretend Synchrony / Goolong (2019) - title: Pretend synchrony: synchronous verification of asynchronous distributed programs - what: Verifies Go distributed programs by automatically rewriting them into an equivalent synchronous program (messages become assignments), then checking ordinary verification conditions with the Z3 solver. Four case studies: two-phase commit, Raft leader election, single-decree Paxos, Multi-Paxos key-value store. - number: manual invariant annotations reduced by 6x versus Dafny - number: check time 1.73 s total vs 1455.84 s in Dafny for the three protocols - number: Paxos 504 lines of Go, 14 loop-invariant lines, 1.51 s; Dafny 72 invariant lines, 1141.35 s - number: Multi-Paxos KV: 847 Go lines, 1.64 s check, 118.5 req/ms, within 1.5-3x of unverified EPaxos code - limits: Safety only, no liveness. Needs structured loops, symmetric process ids, typed channels, pairwise communication and round non-interference; rules out Multi-Paxos stable-leader optimization, Stoppable Paxos and ring topologies such as Chord. - how much was read: parts read - source; notes: Pretend Synchrony (2019) - record id: `pretend-synchrony-goolong-2019` - tla-transmutation (2019) - what: tla-transmutation generates Elixir code and tests from TLA+ specifications. It uses the JSON that Apalache parses. It has separate generators for code, white-box tests and black-box tests. - limits: It is a prototype. The README reports no general proof that the compiler is correct. - how much was read: parts read - source; notes: R04. Elixir generation and Erlang GenServer generation - record id: `tla-transmutation-2019` - Disel (2018) - title: Programming and Proving with Distributed Protocols - what: Proves distributed components and their clients in Coq against protocol descriptions, and composes their contracts. A protocol can be strengthened for one client without redoing the component proofs. - number: about 4,500 lines of framework metatheory - number: two-phase commit core: 997 definition/spec lines and 2,113 proof lines; nine person-days - number: trusted OCaml shim about 250 lines - number: nine person-days for the core two-phase-commit development (§8, PDF p.24) - limits: Safety only. - how much was read: parts read - source; notes: papers and boundaries; notes: Programming and Proving with Distributed Protocols - record id: `disel-2018` - Velisarios (2018) - title: Velisarios: Byzantine Fault-Tolerant Protocols for Verified Distributed Systems - what: It proves agreement for an executable Coq implementation of PBFT: correct replicas return the same reply for the same client and timestamp. Code is extracted to OCaml with a networking and cryptography runtime. - number: PBFT evaluation uses desktops with 16 GB RAM and 8-core 3.40 GHz i7-6700 CPUs - number: Single-machine simulation: 1 million requests, 27.6 microseconds average for f=1 replies - number: Primary failure recovery took around 7 seconds - number: Compared response times with BFT-SMaRt for f=1–3 - limits: The theorem assumes authenticated origins, correct keys, and a bound on the number of faulty nodes. Linearizability, liveness and timeliness are left for future work. The runtime and cryptographic assumptions stay in the trust boundary. - how much was read: parts read - source; notes: Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq; notes: Velisarios: Byzantine Fault-Tolerant Protocols for Verified Distribute - record id: `velisarios-2018` - CertiKOS (2016) - title: CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels - what: CertiKOS specifies an interface and the visible events at each kernel layer. It proves that a module can stand in for its specification in the contexts it allows (this is called contextual refinement). The mC2 kernel is proved in Coq. - number: Under 2 person-years for supporting concurrency - number: 6500 lines of C and x86 assembly - limits: The 2 person-years is the cost of adding concurrency support, not the cost of a whole new kernel. - how much was read: parts read - source; notes: S9 - record id: `certikos-2016` - AWS formal methods (2015) - title: Use of Formal Methods at Amazon Web Services (How Amazon Web Services Uses Formal Methods) - what: AWS engineers used TLA+ and TLC to explore distributed designs and find subtle bugs, including in replication and recovery designs. It is the clearest industrial statement of the gap between model and code. - limits: It checks designs only and does not prove the deployed code correct. The linked manuscript is dated 29 September 2014 and differs from the final publication. - how much was read: parts read - source; notes: P01. How Amazon Web Services Uses Formal Methods; notes: papers - record id: `aws-formal-methods-2015` - seL4 comprehensive (2014) - title: Comprehensive formal verification of an OS microkernel - what: It details seL4's refinement from the abstract spec to the executable design and then to C. It also covers security and binary checks, assumptions and effort. - number: About 20 person-years (py) for the correctness proof, including framework work - limits: Binary verification and hardware assumptions are discussed in Sections 4.7-4.8. Do not carry the historical boundaries over to current versions. - how much was read: parts read - source; notes: S10 - record id: `sel4-comprehensive-2014` - P language (2013) - title: P: Safe Asynchronous Event-Driven Programming - what: P programs are communicating state machines. Some are executable. Others are ghost machines that exist only for specification. The compiler also generates C code, which was used for a Windows 8 driver stack. - limits: Systematic testing leaves liveness checks for future work (PDF p. 9). Foreign functions and runtime integration need separate treatment. Do not read the historical USB result as saying that current AWS code is generated from P. - how much was read: parts read - source; notes: P06. P: Safe Asynchronous Event-Driven Programming - record id: `p-language-2013` - CompCert (2009) - title: Formal verification of a realistic compiler - what: CompCert, a verified C compiler written in Coq. Gives the classic ratio of effort for a verified system. - number: 42000 lines of Coq, approximately 3 person-years - number: 14% compilation algorithms, 10% semantics, 76% correctness proof - number: each compilation pass takes 1500 to 3000 lines for spec and proof - number: 42000 lines of Coq and approximately 3 person-years (that historical version) - limits: Only the paragraph on effort was read. - how much was read: parts read - source; notes: S14 - record id: `compcert-2009` - Refinement mappings (1991) - title: The Existence of Refinement Mappings - what: It shows that suitable refinement mappings (functions from implementation states to spec states) exist once auxiliary variables are added under stated hypotheses. It covers three obstacles: history, prophecy (needing to know the future) and step granularity. - limits: It is a completeness result. It is not an algorithm that finds the variables or the mapping. The notes' author did not fully read the proofs. - how much was read: parts read - source; notes: S2; notes: connecting different descriptions of the same behavior - record id: `refinement-mappings-1991` - Atomkraft - what: A Python package that executes formal-model traces against Cosmos blockchains. - limits: It only connects the model to the implementation for testing. - how much was read: parts read - source; notes: Quint, Apalache, Atomkraft, Modelator - record id: `atomkraft` - Elastic formal models - title: elasticsearch-formal-models - what: The repository has paired TLA+ and Isabelle models of Elasticsearch cluster coordination and data replication. The coordination state maps one-to-one onto the implementation. - limits: The models can differ from the implementations a lot. The one-to-one match holds only for coordination state. - how much was read: parts read - source; notes: R07. etcd/Raft, TiDB, Elastic, and CockroachDB - record id: `elastic-formal-models` - etcd Raft TLA - title: etcd/Raft TLA+ trace-validation integration - what: Build with the with_tla tag so that instrumented Go executions produce events, which are checked against the Raft model. - limits: There is no theorem that the whole code matches the model. Ongaro's original Raft model is a separate artifact. - how much was read: parts read - source; notes: R07. etcd/Raft, TiDB, Elastic, and CockroachDB - record id: `etcd-raft-tla` - Event-B - title: Event-B / Rodin - what: Event-B builds models from sets, with proof obligations and refinement between levels of the model. The code-generation page discusses Tasking Event-B, which aims at executable implementations. - limits: There are several generation approaches, each with different restrictions. Nothing proves in general that Event-B refinements give verified distributed Rust. - how much was read: parts read - source; notes: Alloy and Event-B - record id: `event-b` - Modelator - what: An earlier model-based testing tool. - limits: Its Rust and Go support is deprecated. Keep it as historical evidence. - how much was read: parts read - source; notes: Quint, Apalache, Atomkraft, Modelator - record id: `modelator` - Quint - what: A specification language with simulation and model-checker integrations. The current docs list both TLC and Apalache. - limits: Like TLA+, it checks a model, not the code. - how much was read: parts read - source; notes: Quint, Apalache, Atomkraft, Modelator - record id: `quint` - _refinement - title: _refinement (accompanying material for 'A Tale of Two Refinements') - what: This is a chat-driven refinement of a TLA+ blueprint into multithreaded Rust, using an LLM (Gemini 2.5 Pro). It includes the steps, the chat history and code-review notes. - limits: The README shows no proof, no Verus, and no model checker output. The refinement is informal and checked by reading. The notes did not open the steps and chat files. - how much was read: parts read - source - record id: `refinement` - tla-rs - what: Ports the AutoMan workflow to Rust and Verus. In the RSL and Raft theorems the review notes inspected, finite behaviors of the distributed model are proved to refine an abstract spec. The Raft theorem maps behavior to an abstract behavior of the committed log. - limits: It covers safety correspondence only, with no theorem about eventual progress. Collection helpers are marked external_body, so their contracts are not checked against their bodies. The scheduler, unsafe syscall glue, identity and TLS are outside the body proofs. Verification counts and benchmarks are the authors' reports, which the review notes did not reproduce. - how much was read: parts read - source; notes: tla-rs primary source audit - record id: `tla-rs` - tla-rust - what: An older tutorial workflow. Write a Rust implementation, then test it with QuickCheck and abstracted RPC and clocks, alongside a TLA+ model. - limits: It is a false positive for 'TLA to Rust'. A person implements by hand with help from the model. It is not a compiler, and it does not prove the generated Rust. - how much was read: parts read - source; notes: R05. Hand-written Rust assisted by TLA+, and other generation leads - record id: `tla-rust` - Don't Trust the Code, Check Its Effects: Runtime Refinement for Regenerated Systems Code Under an Adversarial Generator (2026) - what: A position paper. Generated systems code only plans actions, and a trusted mediator owns the effects. - limits: It bears on the trust story, not on distributed proofs. - how much was read: only abstract or first pages read - source - record id: `don-t-trust-the-2026` - LLM-assisted Verification of Protocol Implementations for Logic Flaws Using TLA+ (2026) - what: A pipeline from code to Protocol Intermediate Language to TLA+ to TLC, with feedback. The abstract reports three logic flaws, including WolfSSL 5.8.2 accepting CertificateVerify before ClientKeyExchange. - number: 3 logic flaws confirmed by the vendor - number: Three logic flaws identified, confirmed by the vendor (abstract) - limits: Only the abstract was available. The human inputs, the scope of the proofs and the method are unverified. - how much was read: only abstract or first pages read - source; notes: Located but full text unavailable; notes: Located but full text unavailable - record id: `llm-assisted-verification-of-2026` - SPECA (2026) - title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols - what: SPECA has an LLM read protocol specs (Ethereum consensus) and write categorized properties. It then audits each client against them. These are not proofs. - number: 15/15 in-scope Fusaka vulnerabilities with expert augmentation, 8/15 automated - number: About 30 per high/medium/low bug
  • limits: The authors say the quality of the generated properties is the main limit.
  • how much was read: only abstract or first pages read
  • source; notes: specification-anchored auditing
  • record id: speca-2026
• Fortifying Integrity, Traceability, and Operational Efficacy in Blockchain-Based Examination Management Through Formal Verification with TLA+ (2025)
  • what: Models an Ethereum smart contract for exam records in TLA+ (a specification language for state machines), checks it with the TLC model checker for safety and liveness, and maps the TLA+ constructs to Solidity code. Hoare logic (pre- and postconditions) is applied to key functions.
  • limits: Full text not obtained (IEEE paywall, no open copy found by Unpaywall or Semantic Scholar); only the abstract was read, so properties checked, state-space size and results are unknown.
  • how much was read: only abstract or first pages read
  • source; notes: TLA+ for a blockchain exam-management contract (2025)
  • record id: fortifying-integrity-traceability-and-2025
• hax / Bert13 (2025)
  • title: Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust
  • what: The developer annotates Rust code and picks a backend prover (F*, ProVerif or SSProve) through the hax pipeline. The authors evaluate it on Bert13, a Rust post-quantum TLS 1.3 implementation.
  • limits: The full text was unavailable (HTTP 403). Only the abstract was read, so the scope, numbers and effort are unknown. The abstract makes no liveness claim.
  • how much was read: only abstract or first pages read
  • source; notes: Formal Security and Functional Verification of Cryptographic Protocol
  • record id: hax-bert13-2025
• Model-based testing in an actor model (VK.com, Viewstamped Replication variant) (2025)
  • what: It generates an exhaustive test suite that covers all states and transitions of a finite model. It needs no code changes.
  • limits: It only tests.
  • how much was read: only abstract or first pages read
  • source
  • record id: model-based-testing-in-2025
• Rust guard refinement (2025)
  • title: A Refinement Methodology for Distributed Programs in Rust
  • what: The author’s abstract says it combines guards, locally inductive invariants and Rust ownership in a library usable with an off-the-shelf verifier. The case study is a concurrent Memcached.
  • limits: The notes’ author read only the abstract. The proof boundary, the verifier and the effort are unaudited. It is not necessarily based on Verus.
  • how much was read: only abstract or first pages read
  • source; notes: A Refinement Methodology for Distributed Programs in Rust
  • record id: rust-guard-refinement-2025
• Sonic (2025)
  • title: Formal Model Guided Conformance Testing for Blockchains
  • what: It runs a formal model and the real client in a deterministic simulator, in two workflows: from model to code traces, and from code to model.
  • limits: It is tested only. The model language was not confirmed.
  • how much was read: only abstract or first pages read
  • source
  • record id: sonic-2025
• Verified SCION router (2025)
  • title: Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
  • what: From the authors’ abstract: network-wide protocol and security refinements in Isabelle/HOL are soundly linked to a proof about a Go production router. The proof covers freedom from crashes, freedom from data races, and adherence to the concrete model. The code is from an independent dev team.
  • limits: Only the abstract and the repo were read. Numeric effort and exactly which files were verified are unaudited.
  • how much was read: only abstract or first pages read
  • source; notes: Protocols to Code: Formal Verification of a Secure Next-Generation Int
  • record id: verified-scion-router-2025
• Cedar (2024)
  • what: The AWS authorization language Cedar. It is modeled in Lean with proofs, implemented in Rust, and the Rust is tested against the model by comparing their outputs (differential testing).
  • number: Search-result summary: 4 bugs found by verification, 21 more by testing (unchecked)
  • limits: Not distributed.
  • how much was read: only abstract or first pages read
  • source
  • record id: cedar-2024
• HDBIP (2018)
  • title: Facilitating the Implementation of Distributed Systems with Heterogeneous Interactions
  • what: Introduces HDBIP, an extension of BIP supporting multiparty and direct asynchronous send/receive interactions, with correct-by-construction C++/MPI code generation. A distributed two-phase-commit case study compares execution time and code size against regular BIP.
  • number: Evaluation uses four Ubuntu 16.04 machines with 8 cores and 32 GB RAM each
  • number: Varies transactions 20,000–200,000 with 10 resource managers, and resource managers 2–20 with 10,000 transactions
  • number: HDBIP implementation drastically outperforms regular BIP in the reported two-phase-commit experiments
  • limits: The case study targets MPI-generated C++ and two-phase commit; the paper’s future work includes fault tolerance. The correctness argument concerns the generated interaction implementation, not a machine-checked end-to-end proof.
  • how much was read: only abstract or first pages read
  • source
  • record id: hdbip-2018
• ABS-to-Haskell (2016)
  • title: A Formal, Resource Consumption-Preserving Translation of Actors to Haskell
  • what: Defines a formal translation of a cooperative-scheduling actor-language subset (ABS) to a continuation-based Haskell representation. A simulation theorem establishes trace soundness and a corollary establishes resource-consumption preservation; experiments compare runtime and executed steps on ABS benchmarks.
  • number: Experimental inputs n=500–5000 with 20 runs per value
  • number: Benchmarks include O(n), O(n log n), and O(n²) programs
  • number: The authors report matching growth of runtime and executed steps and no compilation overhead under their cost model
  • limits: The translation fixes a round-robin object/process order and therefore proves soundness but not trace completeness. The model omits full ABS features and nondeterministic scheduling; low-level Haskell garbage-collection costs are future work.
  • how much was read: only abstract or first pages read
  • source
  • record id: abs-to-haskell-2016
• Automated Verification of RPC Stub Code.
  • what: Formal verification has been successfully applied to provide strong correctness guarantees of software systems, but its application to large code bases remains an open challenge. The technique of component-based software devel- opment, traditionally employed for engineering benefit, also aids reasoning about such systems. While there exist compositional verification techniques that lever- age the separation implied by a component system architecture, they implicitly rely on the component platform correctly implementing the isolation and com- position semantics they assume.
  • limits: Read from the saved open PDF; this record uses the abstract/opening section and preserves the exact extracted quote below.
  • how much was read: only abstract or first pages read
  • source
  • record id: automated-verification-of-rpc
• Automating Cryptographic Protocol Language Generation from Structured Specifications.
  • what: latter is a manual refinement from the specification language, that is Security of cryptographic protocols can be analysed by creating often a mix of maths and natural language, to a formal language of arXiv:2105.09150v2 [cs.CR] 5 Apr 2022 a model in a formal language and verifying the model in a tool. choice, with limited semantics, that consequently may only capture All such tools focus on the last part of the analysis, verification, a subset of the initial specification. and the interpretation of the specification is only explained in The model interpreting the design of a protocol is the first math- papers.
  • how much was read: only abstract or first pages read
  • source
  • record id: automating-cryptographic-protocol-language
• Compiling CAO: From Cryptographic Specifications to C Implementations
  • what: . We present a compiler for CAO, an imperative DSL for the cryptographic domain. The tool takes high-level cryptographic algorithm specifications and translates them into C implementations through a series of security-aware transformations and optimizations.
  • how much was read: only abstract or first pages read
  • source
  • record id: compiling-cao-from-cryptographic
• Discourje: Run-Time Verification of Communication Protocols in Clojure - Live at Last.
  • what: . Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (com- munication deadlock freedom) of implementations relative to specifica- tions.
  • how much was read: only abstract or first pages read
  • source
  • record id: discourje-run-time-verification
• Discourje: Runtime Verification of Communication Protocols in Clojure.
  • what: . This paper presents Discourje: a runtime verification frame- work for communication protocols in Clojure. Discourje guarantees safety of protocol implementations relative to specifications, based on an ex- pressive new version of multiparty session types.
  • how much was read: only abstract or first pages read
  • source
  • record id: discourje-runtime-verification-of
• Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM.
  • what: This paper introduces the QCheck-STM plugin for Ortac, a framework for dynamic verification of OCaml code. Ortac/QCheck-STM consumes OCaml module signatures annotated with behavioural specific- ation contracts expressed in the Gospel language, extracts a functional model of a mutable data structure from it, and generates code for auto- mated runtime assertion checking. We report on the implementation of the tool, the structure of the generated code, and on errors found in established OCaml libraries.
  • how much was read: only abstract or first pages read
  • source
  • record id: dynamic-verification-of-ocaml
• Formal Verification of Hardware Synthesis.
  • what: . We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEath- erweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions.
  • how much was read: only abstract or first pages read
  • source
  • record id: formal-verification-of-hardware
• Formally Verified EVM Block-Optimizations
  • what: . The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimiz- ers to enhance efficiency may introduce bugs and compromise security. Our focus is on EVM (Ethereum Virtual Machine) block-optimizations, which enhance the efficiency of jump-free blocks of opcodes by eliminat- ing, reordering and even changing the original opcodes.
  • how much was read: only abstract or first pages read
  • source
  • record id: formally-verified-evm-block
• Integrated Environment for Verifying and Running Distributed Components
  • what: . This paper targets the generation of distributed applica- tions with safety guarantees. The proposed approach starts from graph- ical specification formalisms allowing the architectural and behavioral description of component systems.
  • how much was read: only abstract or first pages read
  • source
  • record id: integrated-environment-for-verifying
• JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java
  • what: . We present “Verified JavaBIP”, a tool set for the verification of JavaBIP models. A JavaBIP model is a Java program where classes are considered as components, their behaviour described by finite state machine and synchronization annotations.
  • how much was read: only abstract or first pages read
  • source
  • record id: javabip-meets-vercors-towards
• Kmclib: Automated Inference and Verification of Session Types from OCaml Programs.
  • what: . Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrin- sically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type.
  • how much was read: only abstract or first pages read
  • source
  • record id: kmclib-automated-inference-and
• ModelPlex: verified runtime validation of verified cyber-physical system models
  • what: Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world.
  • how much was read: only abstract or first pages read
  • source
  • record id: modelplex-verified-runtime-validation
• Proof-Producing Synthesis of CakeML from Monadic HOL Functions
  • what: We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, excep- tions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial exam- ples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance.
  • how much was read: only abstract or first pages read
  • source
  • record id: proof-producing-synthesis-of
• Proof-producing translation of higher-order logic into pure and stateful ML
  • what: The higher-order logic found in proof assistants such as Coq and various HOL systems provides a convenient setting for the development and verification of functional programs. However, to ef- ficiently run these programs, they must be converted (or ‘extracted’) to functional programs in a programming language such as ML or Haskell. With current techniques, this step, which must be trusted, relates similar looking objects that have very different semantic definitions, such as the set- theoretic model of a logic and the operational semantics of a programming language.
  • how much was read: only abstract or first pages read
  • source
  • record id: proof-producing-translation-of
• Q: A Sound Verification Framework for Statecharts and Their Implementations
  • what: C. Rawlings. 2022.
  • how much was read: only abstract or first pages read
  • source
  • record id: q-a-sound-verification
• Towards Verified Scalable Parallel Computing with Coq and Spark
  • what: SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e.
  • how much was read: only abstract or first pages read
  • source
  • record id: towards-verified-scalable-parallel
• Unleashing the Power of LLM to Infer State Machine From the Protocol Implementation
  • what: —State machines are essential for enhancing proto- significantly discrepant FSMs, and these discrepancies are col analysis to identify vulnerabilities. However, inferring state often hotspots for vulnerabilities. Therefore, FSMs extracted machines from network protocol implementations is challenging from specific protocol implementations are more accurate than due to complex code syntax and semantics.
  • how much was read: only abstract or first pages read
  • source
  • record id: unleashing-the-power-of
• Verified High Performance Computing: The SyDPaCC Approach
  • what: The SyDPaCC framework for the Coq proof assistant is based on a transfor- mational approach to develop verified efficient scalable parallel functional programs from specifications. These specifications are written as inefficient (potentially with a high computational complexity) sequential programs using some easily understandable predefined sequential function. We obtain efficient parallel programs implemented us- ing algorithmic skeletons that are higher-order functions implemented in parallel on distributed data structures.
  • how much was read: only abstract or first pages read
  • source
  • record id: verified-high-performance-computing
• Emerald Quint post (2026)
  • title: Model-Based Testing EVM networks with Quint and AI
  • what: An AI reads the Emerald code and writes a Quint spec, and humans refine it. The AI then generates most of the driver that replays model traces on the Rust code and compares state.
  • number: Three validated invariants incl. agreement on decided blocks
  • number: Coverage about 80% at the application layer
  • number: Found a leak of completed streams
  • limits: It gives no model version, no autonomous success rate, and no proof for unbounded cases. The consensus and execution engines are not modeled.
  • how much was read: reading depth not recorded
  • source; notes: Quint: production case studies, not a measured proof benchmark
  • record id: emerald-quint-post-2026
• lemmafit (2026)
  • title: Introducing lemmafit: A Verifier in the AI Loop
  • what: From an ordinary request, Claude Code writes structured requirements, Dafny state and action code, and lemmas. A file watcher runs Dafny. The verified logic is compiled into a TypeScript API that React uses.
  • limits: It covers logic without side effects, in new React/TypeScript apps. The human must review the English spec. The agent model and success rate are not reported. It has no result on autonomous distributed protocols or liveness.
  • how much was read: reading depth not recorded
  • source; notes: lemmafit: Claude Code writes the specification, implementation, and pr
  • record id: lemmafit-2026
• LemmaScript (2026)
  • title: LemmaScript: A Verification Toolchain for TypeScript via Dafny
  • what: Contracts are written as TypeScript comments. The tool derives Dafny or Lean/Velvet models from them and verifies those, while ordinary TypeScript still runs as usual. Example repositories verify shared client/server cores, such as a quota booking app and a rate limiter.
  • number: Quorum scheduler 100 Dafny VCs; quota booking 80; Hono rate limiter 23; Henri agent core 48 (README)
  • limits: The author warns of gaps between the model and the real semantics. I/O, auth, network and UI stay trusted. No agent model or success rate. The corpus is ‘not an agentic proof benchmark’.
  • how much was read: reading depth not recorded
  • source; notes: LemmaScript and Velvet: verified TypeScript components, including shar
  • record id: lemmascript-2026
• SysMoBench blog (2026)
  • title: Can LLMs model real-world systems in TLA+?
  • what: The post explains concrete modeling mistakes. Models copy textbook Raft instead of the implementation’s own voting. Or they merge atomic guards and erase ZooKeeper’s higher-epoch transition.
  • limits: Do not mix its newer aggregate results with the paper’s table.
  • how much was read: reading depth not recorded
  • source; notes: SysMoBench: real code exposes failures hidden by puzzle benchmarks
  • record id: sysmobench-blog-2026
• Malachite Quint post (2025)
  • title: Reliable Software in the LLM Era
  • what: A protocol refactor of Fast Tendermint (Malachite). AI updates the Quint spec. Humans check the reachable behaviors and properties. AI changes the code and writes glue for model-based tests.
  • number: About 2 days for spec modification and validation, about one week for code and testing
  • number: Spec validation found two small bugs in the English spec in one afternoon
  • limits: An agent-assisted refactor. The agent did not invent the protocol, and there is no unbounded proof. No measured success rate.
  • how much was read: reading depth not recorded
  • source; notes: Quint: production case studies, not a measured proof benchmark
  • record id: malachite-quint-post-2025
• DistAlgo (2012)
  • title: From Clarity to Efficiency for Distributed Algorithms
  • what: DistAlgo lets you write queries over message history directly. It compiles them, and makes them incremental, into efficient Python.
  • limits: It is a paper about a language and its optimization. It gives no machine-checked guarantee of safety or liveness.
  • how much was read: reading depth not recorded
  • source; notes: From Clarity to Efficiency for Distributed Algorithms
  • record id: distalgo-2012
• Civl
  • title: Civl verifier (official site)
  • what: A verifier built on layers of refinement (each layer a simpler or more detailed version of the one next to it) and structured programs. An SMT solver discharges the checking conditions. Its samples include Paxos, 2PC and Chang-Roberts.
  • limits: The test suite is a repository that keeps changing. An evaluation needs a pinned commit.
  • how much was read: reading depth not recorded
  • source; notes: Civl and inductive sequentialization
  • record id: civl
• Verifier-supervised fine-tuning for Rust/Verus: vericoding dataset (restricted) (2026)
  • what: A Zenodo record for a training dataset of Rust/Verus verified-code tasks used to fine-tune a code model with the verifier as the supervision signal. Only the record’s metadata could be read: the files are under embargo until 2026-12-31 and the record has no listed files.
  • limits: Blocked: no full text exists and the data is embargoed (‘access_right’: ‘embargoed’, embargo_date 2026-12-31) with the author listed as ‘Anonymous’ (double-blind review). Everything here comes from the record’s description and keywords; content, size, and results are unknown.
  • how much was read: not read; title and metadata only
  • source; notes: Verifier-supervised fine-tuning for Rust/Verus dataset (2026)
  • record id: verifier-supervised-fine-tuning-2026
• AWS correctness practices (2025)
  • title: Systems Correctness Practices at Amazon Web Services
  • what: The paper was not read. Search summaries say it covers P, model checking, fuzzing, property-based testing, fault injection and simulation, with formal specs used as test oracles (the source of expected answers).
  • limits: Fetching the paper returned HTTP 403. The claims are unverified search summaries.
  • how much was read: not read; title and metadata only
  • source; notes: P02. Systems Correctness Practices at Amazon Web Services
  • record id: aws-correctness-practices-2025
• iMocket (2025)
  • title: iMocket: model checking guided incremental testing
  • what: Re-tests only the states affected by code and spec changes.
  • number: Reduces test cases by 74.83% on 12 change scenarios from three systems
  • limits: Tested only. Seen as a snippet.
  • how much was read: not read; title and metadata only
  • source
  • record id: imocket-2025
• Model Checking Guided Incremental Testing for Distributed Systems (2025)
  • what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
  • limits: Not read. Claims are unverified.
  • how much was read: not read; title and metadata only
  • source
  • record id: model-checking-guided-incremental-2025
• Proving Correctness of Parallel Implementations of Transition System Specifications (2023)
  • what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
  • limits: Screened as unreachable: the downloaded file could not be extracted.
  • how much was read: not read; title and metadata only
  • source
  • record id: proving-correctness-of-parallel-2023
• PGo overview talk (2022)
  • what: YouTube metadata identifies a UBC Systopia recording titled “Compiling Distributed System Models Into Implementations with PGo (Shayan Hosseini)”.
  • limits: Only metadata retrieved; not transcribed.
  • how much was read: not read; title and metadata only
  • source
  • record id: pgo-overview-talk-2022
• PGo talk (2022)
  • title: PGo conference talk
  • what: YouTube metadata identifies a TLA+ Foundation recording titled “Compiling Distributed System Models into Implementations with PGo - Hackett et al.”
  • limits: Only official video metadata was retrieved; the recording was not transcribed in this pass.
  • how much was read: not read; title and metadata only
  • source
  • record id: pgo-talk-2022
• Oracle TLA+ talk (2021)
  • title: Reverse Engineering with TLA+
  • what: YouTube metadata identifies a TLA+ Foundation recording titled “Reverse Engineering with TLA+ — Calvin Loncaric, Oracle”.
  • limits: Only metadata retrieved; not transcribed.
  • how much was read: not read; title and metadata only
  • source
  • record id: oracle-tla-talk-2021
• Effective Concurrency Testing for Distributed Systems (2020)
  • what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
  • limits: Not read. Claims are unverified.
  • how much was read: not read; title and metadata only
  • source
  • record id: effective-concurrency-testing-for-2020
• Formal specification and verification of a broadcasting protocol: a refinement-based approach (2020)
  • what: Listed as an unread search lead from OpenAlex. The notes give only its title, year and DOI.
  • limits: Not read. Claims are unverified.
  • how much was read: not read; title and metadata only
  • source
  • record id: formal-specification-and-verification-2020
• Compiling distributed system specifications into implementations (2019)
  • what: This is an unread search lead from OpenAlex. The notes give only its title, year and DOI.
  • limits: The review notes did not read it. The claims are unverified.
  • how much was read: not read; title and metadata only
  • source
  • record id: compiling-distributed-system-specifications-2019
• KEVM (2018)
  • title: KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine
  • what: A formal semantics of the EVM in the K framework. The notes inspected only the repository README. It names concrete execution on LLVM and symbolic execution in Haskell.
  • limits: The full paper was not obtained (links returned 404/403). No paper-level results are used.
  • how much was read: not read; title and metadata only
  • source; notes: Bytecode-semantics prerequisites: repository evidence and retrieval ga; notes: Bytecode-semantics prerequisites: repository evidence and retrieval ga
  • record id: kevm-2018
• Stateright
  • what: The same actor code can be model checked and also run over UDP. Properties include “eventually” (liveness).
  • limits: It is bounded model checking, not proof. The review notes saw only a search snippet.
  • how much was read: not read; title and metadata only
  • source
  • record id: stateright

Last edited: 2026-10-31