REVIEW 3 major objections 5 minor 17 references
Correctness Witnesses with Function Contracts
T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash
Pith's one-line read Correctness witnesses can now encode function contracts
desk verdict A clean, well-scoped design paper extending witness format 2.0 with function contracts; the main caveat is the single-entry validity semantics, which the paper acknowledges but the abstract overstates. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central machinery is a new entry type `function_contract` placed inside the `invariant_set`, together with a new expression format `acsl_expression`. The entry has optional `requires` and `ensures` clauses that default to true; the format allows `\result` for the return value and `\old(x)` or `\at(x, Pre)` for the values of globals and parameters in the pre-state of the current function call. This machinery carries the argument by giving validators a source-level contract to check at function entry and exit, and by giving verifiers a way to export relational summaries that cannot be expressed as location or loop invariants.
What would settle it
Take a program with two entry points, such as `main` and a second start function, where function `f` satisfies its `requires` and `ensures` clauses on all calls reachable from `main` but violates `ensures` when called from the second entry point; under the paper's semantics the witness is valid, while under a definition quantifying over all calls from all entry points it is invalid.
Extended reading notes
Core claim
The paper claims that witness validity can be defined for function contracts by requiring each `requires` clause to hold before the first statement of the function body and each `ensures` clause to hold after every return, for every call reachable from `main`, with `\old(x)` evaluated in the pre-state and `\result` in the post-state. With this semantics, the extension is backward compatible for verifiers and forward compatible for validators: an empty witness remains valid, every version 2.0 witness is accepted, and validators can check the new entries or return `unknown` when a deductive validator cannot establish correctness.
Load-bearing premise
The whole validity definition is anchored to program executions that start in `main`, so a contract may be certified as valid even if it fails for a call made from another entry point, a library, or differently linked code.
Editorial extensions
If this is right
- Any witness in version 2.0 remains valid, and the empty witness remains valid, so the change does not break existing verifiers or validators.
- Validators can handle `c_expression` contracts by treating `requires` like a location invariant at function entry and `ensures` like a check after the returned expression is evaluated.
- Supporting `acsl_expression` can be implemented by instrumenting ghost variables that record `\old(x)`, `\at(x, Pre)`, and `\result`.
- Deductive verifiers can validate witnesses with function contracts as modular inductive certificates; if they cannot establish correctness, the validator must answer `unknown` rather than reject the witness.
- The format still cannot express heap and pointer invariants or data abstraction, so some correctness arguments remain inexpressible.
Reading between the lines
- If the format is adopted widely, witness producers could increasingly emit modular proof artifacts, potentially shifting cooperative verification from whole-program invariants toward compositional summaries.
- The single-entry semantics means that two witnesses for the same function could disagree when the function is linked under different calling contexts; an alternative semantics quantifying over all entry points would make contracts absolute, at the cost of harder validation.
- The restriction of `\old` to variables and `\at` to `Pre` keeps parsing simple, but a straightforward extension to arbitrary expressions would align the witness format with full ACSL and may be needed for realistic heap-aware contracts.
- A testable prediction is that adding function-contract witnesses to a validator should shorten re-verification time on modular programs relative to location invariants, because the validator can check the summary instead of re-discovering it.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes an extension to the software correctness witness format 2.0 that adds a new entry type 'function_contract' with optional 'requires' and 'ensures' clauses, and an 'acsl_expression' expression format supporting \result, \old, and \at(_, Pre). The syntax and a semantics are given: a function contract is valid if its requires and ensures clauses hold at every call of the function in every program execution that starts in main. The paper claims backward compatibility with witness format 2.0 and argues that the extension enables exchange of information with tools that require function contracts, such as deductive verifiers. It also discusses validation strategies and remaining limitations involving heap, pointers, and data abstraction.
Significance. If the proposed extension worked as claimed, it would address a genuine gap in the witness format: correctness witnesses in version 2.0 cannot express relational pre/post-conditions of functions. The design is presented with concrete examples and a careful syntax discussion, and the paper is transparent about several limitations. However, the central claim that the format allows exchange with tools that require function contracts is currently not supported, because the validity semantics in Section 3 defines a whole-program, single-entry property rather than a modular, caller-independent function contract. This is not merely a presentation issue: it changes what a witness certifies and makes the proposed 'function contract' incompatible with standard contract semantics used by deductive verifiers. The paper's own Section 4 note that the entries 'do not necessarily encode a modular proof' partially acknowledges this, but the abstract and introduction still overstate the contribution. With a revised semantics or appropriately qualified claims, the proposal could be a useful step toward richer correctness witnesses.
major comments (3)
- [Section 3, 'Semantics'] The validity definition for requires and ensures clauses is not a function-contract semantics in the standard assume-guarantee sense. A requires clause is defined to be valid only if it evaluates to true at every call reachable from main, rather than being an assumption under which the ensures clause must hold. Consequently, a witness can be valid even when the encoded contract is false for a call that satisfies the precondition but is not reachable from main. Concretely, let f return 1 normally but return 0 when its argument is 2, and let the witness contain requires x > 0 and ensures \result == 1. If main only calls f(1), the witness is valid under the paper's definition, yet the contract is false for the precondition-satisfying call f(2). A modular deductive verifier such as Frama-C would not accept this pair as a valid contract. Since the abstract and Section 1 claim that the format allows 'exchange of information with tools that require function contracts,' this semantic mismatch is load-bearing and must be addressed: either change the semantics to a caller-independent, assume-guarantee definition, or substantially weaken the exchange claim in the abstract and introduction.
- [Section 3, definition of 'initial state'] The validity of every entry is defined over 'every program execution starting in an initial state, i.e., starting in main,' but the paper does not say what an initial state is. This matters for programs with nondeterministic functions, uninitialized globals, input parameters, and library functions. Without a precise definition of initial state, the set of executions over which requires and ensures are quantified is not well defined, so the semantics of the new format is incomplete. The paper should either define initial state with respect to the C standard plus the SV-COMP convention for nondeterminism, or state explicitly that the semantics is only a proposal that requires such a definition.
- [Section 3, evaluation of c_expression ensures] For a function contract with format c_expression, the paper says the ensures clause is evaluated 'after every return statement ... before returning to the caller,' but it does not specify the variable environment at that point. Since C function parameters are local variables, a parameter may have been modified in the function body, and it is unclear whether a mention of that parameter in the ensures clause denotes its value before the call, its final value in the callee frame, or something else. The paper only clarifies this for acsl_expression, where a parameter 'always evaluates to the value before the call' and \old is available. The missing clarification affects the meaning of every c_expression ensures clause and should be resolved with an explicit rule, for example by stating that c_expression ensures clauses are evaluated in the caller's state after the return value has been computed, or by defining the callee-frame evaluation precisely.
minor comments (5)
- [Section 3, first paragraph] There is a duplicated word in 'for every function call of f in in every program execution'; it should read 'in every program execution.'
- [Section 2, function_contract syntax] The paper requires that clauses be 'side effect-free C expressions,' but side-effect-freeness is a semantic property, not a syntactic one. Since the format is meant to be machine-checkable, the syntax should either define a syntactic fragment that guarantees absence of side effects or specify how side effects are detected and rejected.
- [Section 4, 'Compatibility'] The terms 'backwards compatible for verifiers' and 'forwards compatible for validators' are used without definition. A brief explanation of what each direction means would help readers who are not familiar with the witness-format terminology.
- [Table 1 and Section 2] The table says the acsl_expression format 'is always the case when keywords like \old and \result are used,' but it is not stated whether the 'format' field is mandatory and what a validator should do if it is absent while the expression contains an ACSL keyword. Making the format field required and defining validation of this consistency would remove ambiguity.
- [Section 2, multiple contracts] The paper states that multiple function contracts are allowed for the same function and 'all need to be valid for the witness to be valid,' but it does not say whether multiple contracts for one function are interpreted as a conjunction or as independent certificates. A one-sentence clarification would prevent misinterpretation by tool implementers.
Circularity Check
No significant circularity: the extension to witness format 2.0 is defined and specified in this paper, not derived from its own inputs.
full rationale
The paper's central claim is a format proposal: it adds a function_contract entry type and an acsl_expression format to witness format 2.0, and it defines the validity semantics for these entries in Section 3. The only input that could look load-bearing is the citation to witness format 2.0 [1], which is prior published work by overlapping authors, but the new entry type, the acsl_expression syntax, and the requires/ensures validity semantics are introduced and specified in this paper rather than imported as an unsupported premise. Backward compatibility is established by explicit construction: requires and ensures default to true, making version 2.0 witnesses valid in the extended format by definition; this is not a circular prediction but a stated design property. No parameter is fitted, no quantity is predicted from a subset of data, and no uniqueness theorem is invoked to force a choice. The main-only validity semantics ('starting in an initial state, i.e., starting in main') is a real scope limitation: a witness entry can be valid even though the encoded contract would be false for calls not reachable from main, and the paper itself acknowledges in Section 4 that witnesses 'do not necessarily encode a modular proof.' That weakens the claimed exchange with modular deductive verifiers, but it is an honestly stated limitation of the proposed semantics, not circularity. No derivation chain in the paper reduces to its own inputs.
Assumptions & free parameters
assumptions (4)
- domain assumption Programs are single-entry and all function calls considered occur in executions starting in main.
- domain assumption requires and ensures expressions are side-effect free and contain only globals and parameters, plus \result, \old, or \at(_, Pre) in acsl_expression format.
- domain assumption A unique pre-state exists for each function call, relative to which \old, \at(_, Pre), and parameter values in acsl ensures are evaluated.
- domain assumption The ACSL constructs \result, \old, and \at(_, Pre) can be assigned the restricted semantics given in Section 3.
Cite this review
Pith. "Pith review of Correctness Witnesses with Function Contracts." pith.science (2026). https://pith.science/paper/W52ZSDCN
@misc{pith2026250112313,
author = {Pith},
title = {Pith review of: Correctness Witnesses with Function Contracts},
year = {2026},
howpublished = {\url{https://pith.science/paper/W52ZSDCN}},
note = {Machine review of arXiv:2501.12313}
}
read the original abstract
Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing other tools to reproduce the verification results. Correctness witnesses in the current format (version 2.0) allow only for the encoding of loop and location invariants using C expressions. This limits the correctness arguments that verifiers can express in the witness format. One particular limitation is the inability to express function contracts, which consist of a pre-condition and a post-condition for a function. We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts. Our extension includes support for several features inspired by ACSL (\result, \old, \at). This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.
Figures
Reference graph
Works this paper leans on
-
[1]
Ayaziová, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strejček, J.: Software verification witnesses 2.0. In: Proc. SPIN. pp. 184–203. LNCS 14624, Springer (2024). https://doi.org/10.1007/978-3-031-66149-5_11 Correctness Witnesses with Function Contracts 9
-
[2]
Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C specification language version 1.21 (2024), available at https://frama-c.com/download/acsl-1.21.pdf
work page 2024
- [3]
- [4]
- [5]
- [6]
- [7]
-
[8]
Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Proc. SEFM. p. 111–128. LNCS 13550, Springer (2022). https://doi.org/10.1007/978-3-031-17108-6_7
Show all 17 references
-
[9]
In: Proc
Beyer, D., Strejček, J.: Case study on verification-witness validators: Where we are and where we go. In: Proc. SAS. pp. 160–174. LNCS 13790, Springer (2022). https://doi.org/10.1007/978-3-031-22308-2_8
2022 doi
-
[10]
In: Proc
Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA (1). pp. 143–167. LNCS 12476, Springer (2020). https://doi.org/10.1007/978-3-030-61362-4_8
2020 doi
-
[11]
Blom, S., Huisman, M.: The vercors tool for verification of concurrent programs. In: FM. LNCS, vol. 8442, pp. 127–131. Springer (2014).https://doi.org/10.1007/ 978-3-319-06410-9_9
2014
-
[12]
In: Proc
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Proc. SEFM. pp. 233–247. Springer (2012).https://doi.org/10. 1007/978-3-642-33826-7_16
2012
-
[13]
In: Proc
Ernst, G., Pfeifer, W., Ulbrich, M.: Contract-lib: A Proposal for a Common In- terchange Format for Software System Specification. In: Proc. ISoLA (3). Lec- ture Notes in Computer Science, vol. 15221, pp. 79–105. Springer (2024).https: //doi.org/10.1007/978-3-031-75380-0_6
2024 doi
-
[14]
Hähnle, R., Huisman, M.: Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools, pp. 345–373. Springer (2019). https://doi.org/10. 1007/978-3-319-91908-9_18
2019
-
[15]
In: Proc
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Proc. NFM. pp. 41–55. LNCS 6617, Springer (2011).https://doi.org/10.1007/ 978-3-642-20398-5_4
2011
-
[16]
In: Proc
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proc. LPAR. pp. 348–370. LNCS 6355, Springer (2010).https://doi.org/10. 1007/978-3-642-17511-4_20
2010
-
[17]
Computer25(10), 40–51 (1992).https: //doi.org/10.1109/2.161279
Meyer, B.: Applying ’design by contract’. Computer25(10), 40–51 (1992).https: //doi.org/10.1109/2.161279
1992 doi
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.