Paper Citation Record · LEDGER

dafny-annotator: AI-Assisted Verification of Dafny Programs

As of 19 August 2026, this Paper Citation Record lists 0 of 0 outbound references and 5 inbound Pith citation observations for arXiv:2411.15143.

A citation records a reference. It does not transfer a finding from one paper to another.

pith.paper-citation-record.v1
2411.15143 v1

Coverage vector

measured 0 of 0 reference resolution

Typed states for the displayed outbound observations.

Source: paper_references, paper_reference_links

measured 5 of 5 standing notices

One-hop event checks from named stored sources.

Source: scholarly_work_events, retraction_status_cache, observed 2026-08-19T06:32:44.657259+00:00

measured 5 of 5 inbound itemization

Pith citing papers itemized under the disclosed page cap.

Source: paper_references, paper_reference_links, observed 2026-08-06T22:10:19.945974Z

measured 0 of 1 external citation measurements

A source-named dated measurement, never combined with another source.

Source: arxiv_reference, observed 2026-07-04T13:49:52.463211Z

Reference resolution

0 of 0 outbound references displayed

verified exact0
verified fuzzy0
unresolved0
parse uncertain0
malformed identifier0
metadata mismatch0

External citation measurements

No source-named external measurement is stored.

Outbound references

No outbound reference observations are available for this paper version.

Pith citing papers

Observation 77098d97-8aa7-4a23-9456-0ae2eec6f4d3 · inbound

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny cites this paper.

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny dafny-annotator: AI-Assisted Verification of Dafny Programs

Reference 15

Resolution: unresolved; no resolver link, observed 2026-08-06T22:10:19.945974Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 9e12d4bf-8609-4b5f-b343-b3ba71f9a748 · inbound

Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny cites this paper.

Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny dafny-annotator: AI-Assisted Verification of Dafny Programs

Reference 60

Resolution: unresolved; no resolver link, observed 2026-08-06T15:20:15.513785Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation 3c1995e0-7255-439c-b94d-dcd8e9a7e146 · inbound

An Empirical Study of LLM-Generated Specifications for VeriFast cites this paper.

An Empirical Study of LLM-Generated Specifications for VeriFast dafny-annotator: AI-Assisted Verification of Dafny Programs

Reference 31

Resolution: verified exact; arxiv_id, observed 2026-07-04T13:49:52.464772Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-19T06:32:44.657259+00:00.

Observation 7220cdfd-d661-4f2a-9dee-eec5d480cf42 · inbound

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability cites this paper.

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability dafny-annotator: AI-Assisted Verification of Dafny Programs

Reference 22

Resolution: unresolved; no resolver link, observed 2026-07-13T03:34:35.116630Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

Observation ff2bbf48-e87e-4c78-a83f-baf627f1c728 · inbound

Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification cites this paper.

Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification dafny-annotator: AI-Assisted Verification of Dafny Programs

Reference 43

Resolution: unresolved; no resolver link, observed 2026-07-14T12:52:50.844575Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.