Formal languages are widely used in software engineering to specify and verify program properties. Because their mathematical notation and logic are hard to read, developers often rely on natural-language documentation to understand the functions in formal libraries. Yet a documentation statement can be provably true and still hold after the function's behavior changes. We call a statement's dependence on the function's specific behavior attribution, and we give a method to check it. We design and implement DocAuth, a documentation-generation method that uses attribution to decide what to publish and attaches to each published sentence the formal property recovered from it, together with checkable evidence. On 150 functions from the Community Books library of the ACL2 theorem prover, three large language models produce proved but non-attributable properties for about a third of the functions. DocAuth matches or exceeds the attribution rate of a mutation-based filter while delivering 37% more attributable sentences. Compared with a pipeline that checks truth alone, it raises the share of published sentences that a second model confirms as attributable from 82.9% to 94.7%. These results show that provable truth does not guarantee that documentation reflects what a function actually does. Attribution complements truth as a criterion for generating and evaluating documentation for formal libraries.
Figures & tables
Measure
Unit of decision
Reference
Question answered
Can reject Figure 1 statements
Provability ( Ma et al., 2025 )
Individual property
Original target
Can the property be proved?
✗
Mutation discrimination ( Endres et al., 2024 ; Amaral et al., 2026 ; Goldweber et al., 2024 )
Property or whole specification
Selected code mutants
Which tested implementations does it rule out?
Vacuity and semantic dependence ( Beer et al., 2001 ; Podgurski and Clarke, 1990 ; Chockler et al., 2008 )
Property or program part
Changes to a subformula or program part
Does the conclusion depend on the changed part?
✗
Document–code equivalence ( Eghbali et al., 2026 ; Zeng et al., 2026 )
Entire document or specification
Overall behavior of the original target
Do the two describe the same behavior?
✗
Source support and consistency ( Rashkin et al., 2023 ; Panthaplackel et al., 2021 ; Sun et al., 2024 )
Sentence or comment
Source text or code
Is the statement supported and consistent?
✗
Attribution (ours)
Individual statement
Implementations under the fixed interface
Does it add behavioral information beyond the interface?
✓
Table 1. Attribution compared with existing measures. ✓ guaranteed; depends on the selected variants; ✗ not guaranteed.
Figure 3. The DocAuth workflow The workflow has three stages. During candidate generation, an LLM reads the formal target function and proposes candidate properties. The candidate check first identifies non-attributable properties through an erasure proof, then obtains a target proof and an interface-conforming witness for the remaining properties; these two items form the attribution evidence. Properties that pass the check are rendered as natural-language sentences, from which formal properties are recovered by back-translation and subjected to the sentence recheck; only sentences that pass both checks are published to developers, and everything else is discarded.
Qwen2.5-7B
DeepSeek-v4-flash
GPT-5.6-terra
Human-written
Properties checked
1,743
2,030
2,090
1,068
Checks completed
939
1,215
1,371
466
❶ Attributable
461 (49.1%)
921 (75.8%)
1,209 (88.2%)
409 (87.8%)
False for the target
373 (39.7%)
143 (11.8%)
27 (2.0%)
0 (0.0%)
❷ Non-attributable
80 (8.5%)
77 (6.3%)
72 (5.3%)
20 (4.3%)
❸ No witness found
25 (2.7%)
74 (6.1%)
63 (4.6%)
37 (7.9%)
Table 2. Outcomes of the properties checked on 150 functions
Property source
Attributable
No witness found
Non-attributable
Qwen2.5-7B
68/123 (55.3 %)
1/6 (16.7 %)
0/16
DeepSeek-v4-flash
204/304 (67.1 %)
4/21 (19.0 %)
0/14
GPT-5.6-terra
264/401 (65.8 %)
4/19 (21.1 %)
0/10
Human-written
78/120 (65.0 %)
0/13 (0.0 %)
0/8
Total
614/948 (64.8 %)
9/59 (15.3 %)
0/48
Table 3. Change detection by property source and check outcome
Generator model
Method
Published
Attributable
Cross-model
Interface-only
Interface-only, equivalent to ψ
Qwen2.5-7B
Baseline
575
247
43.0%
26.1%
20.2%
+ LLM judge
404
217
53.7%
34.2%
26.5%
Truth check
376
299
79.5%
62.5%
43.9%
+ LLM judge
359
290
80.8%
63.5%
44.8%
+ mutation filter
265
229
86.4%
64.5%
44.2%
DocAuth
359
317
88.3%
68.0%
46.8%
Table 4. Attributable sentences and attribution rates by generator model and reassessment condition
Figure 6. Sentence attribution rates, pooled over the three models Grouped bar chart. The horizontal axis shows the three reassessment conditions: cross-model, interface-only, and interface-only with equivalence to psi. Each group has six bars, for the baseline, the baseline with LLM judging, truth checking, truth checking with LLM judging, truth checking with mutation filtering, and \tool; error bars are 95% bootstrap intervals clustered by target function. \tool's bar is the tallest in all three groups, at 94.7%, 75.7%, and 52.7%, respectively. Table~\ref{tab:independent} gives the values for each generator model.
Method
Nothing published
≥1 attributable
≥2 attributable
4 attributable
Attributable per document
Attribution rate
Baseline
0.7%
83.3%
65.8%
8.0%
1.90
49.7%
Truth check
16.9%
79.3%
72.0%
30.9%
2.40
82.9%
+ mutation filter
36.4%
62.4%
55.6%
26.4%
1.90
92.0%
DocAuth
18.7%
80.9%
74.7%
40.9%
2.60
94.7%
Table 5. Per-function delivery
Figure 7. Effects of the candidate budget, the search scope, and the number of sentences per function Four line plots in one row. (a) As the candidate budget grows, the share of attributable properties falls for all four property sources. (b) The number of properties still without a witness when the search is limited to a prefix of the alternative implementations drops sharply at the second alternative and keeps falling to the no-witness-found count of the full search. (c, d) With published sentences truncated per function, DocAuth's attribution rate stays above that of truth checking, and the number of attributable sentences delivered by all three methods grows with the number of sentences per function.
Property source
Properties checked
Functions covered
Coverage
Qwen2.5-7B
1,743
114/150
76.0%
DeepSeek-v4-flash
2,030
127/150
84.7%
GPT-5.6-terra
2,090
123/150
82.0%
Human-written
1,068
105/150
70.0%
Table 6. Function coverage by property source
Figure 8. Check outcomes and reasons for unresolved outcomes by property source Each panel has four stacked percentage bars for Qwen2.5-7B, DeepSeek-v4-flash, GPT-5.6-terra, and human-written properties. Panel (a) partitions all checked properties into attributable, false for the target, non-attributable, no witness found, and unresolved. Panel (b) partitions each source's unresolved properties into missing target proofs, missing dependencies or erasure-environment problems, evaluation failures or unmet premises, and other incomplete checks.
Figure 9. Distribution of token usage and total time per function Three violin plots show the distributions of input tokens, output tokens, and total time over the 149 functions. Each plot has a quartile bar and a median dot in the middle, and each function is drawn as a point: dark blue for functions that publish sentences and gray for those that publish nothing. Functions that publish nothing cluster at the low end of total time and also use the fewest input tokens.
School of Mathematical Sciences, Shanghai Jiao Tong University, Shanghai 200240, China · University of California, Berkeley, CA 94720, USA · Zhiyuan College, Shanghai Jiao Tong University, Shanghai 200240, China +4