pith. sign in

arxiv: 2606.23377 · v1 · pith:VUQX6UTSnew · submitted 2026-06-22 · 💻 cs.LO

Partial Automation of Verification Condition Proving for Reflex Programs (Draft)

Artyom Ishchenko , Igor Anureev This is my paper

Pith reviewed 2026-06-26 06:36 UTC · model grok-4.3

classification 💻 cs.LO
keywords Reflex languageverification conditionsdeductive verificationprocess-oriented programmingSMT solversinvariantsannotation languageformal verification
0
0 comments X

The pith

Adding annotations, structural invariants, and SMT solvers to the Reflex verification generator automates proof of some conditions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper targets the practical barrier in deductive verification of large process-oriented programs written in Reflex, where the generator produces too many verification conditions for manual proof to be feasible in industrial systems of hundreds or thousands of processes. It proposes three changes: an annotation language for structured requirements, automatic generation of invariants from program structure, and preliminary use of SMT solvers to discharge conditions without human intervention. A sympathetic reader cares because these steps aim to shrink the manual proof load enough to make formal safety arguments viable for real control systems. If successful, the approach would bridge the gap between full formal methods and the scale of deployed industrial software.

Core claim

The proposed modifications—an annotation language to describe requirements in a structured form, generation of invariants based on the program structure, and SMT solvers for the preliminary attempt to solve the verification conditions—will automate the proof of some verification conditions generated for Reflex programs.

What carries the argument

The modified verification condition generator that incorporates the annotation language, structure-derived invariants, and SMT solver calls to handle preliminary conditions.

If this is right

  • Verification conditions that match the generated invariants or fall within SMT capabilities will be discharged without human input.
  • Requirements expressed through the annotation language will be checked against the program structure automatically.
  • The overall verification workflow for Reflex programs will require fewer manual proof steps than the prior generator.
  • Safety properties of process-oriented control systems become easier to establish at the scale of hundreds of processes.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The technique could be tested on open-source Reflex examples to measure the exact fraction of conditions automated.
  • Similar structural invariant generation might apply to other process-oriented languages beyond Reflex.
  • Integration with existing SMT tools could be extended to handle more complex arithmetic or timing properties common in control systems.

Load-bearing premise

These three modifications will produce a practically useful reduction in the number of verification conditions that still require manual proof for realistic industrial systems.

What would settle it

Apply the modified generator to a Reflex program modeling an industrial system with several hundred processes and count how many verification conditions remain after SMT solving and invariant use; if the remaining count is still too large for manual proof, the claim fails.

Figures

Figures reproduced from arXiv: 2606.23377 by Artyom Ishchenko, Igor Anureev.

Figure 1
Figure 1. Figure 1: Modified algorithm of VCG. The verification process begins by parsing the annotated program into an abstract syntax tree (AST). From this AST, a control-flow graph (CFG) of the program is constructed. In parallel with CFG construction, the annotation parser processes user-provided annotations, translates them into an internal logical representation, and associates them with the corresponding program statem… view at source ↗
read the original abstract

Process-Oriented Programming is a software development approach that emphasizes the management of control systems through abstractions of processes and their states, enabling these systems to be described in terms of real physical processes. This native description of control is particularly important for industrial systems consisting of hundreds or thousands of processes. For such systems, safety is critical. To ensure the reliability and safety of these systems, formal verification methods must be applied. One such method is deductive verification, which involves formalizing programs and their requirements as logical formulas, known as verification conditions. Proving these conditions confirms that the program meets its requirements. The automatic generation of verification conditions is performed by a specialized software tool called a verification condition generator. We previously proposed a verification condition generator for the Reflex language. However, it generates too many verification conditions, making their manual proof impossible. This paper proposes modifications to the verification condition generator aimed at automating the proof of some of these conditions. These modifications include introducing an annotation language to describe requirements in a structured form, generating invariants based on the program structure, and using SMT solvers for the preliminary attempt to solve the verification conditions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The manuscript proposes three modifications to an existing verification-condition generator for the Reflex language: (1) an annotation language for expressing requirements in structured form, (2) automatic generation of invariants derived from program structure, and (3) preliminary discharge of verification conditions by SMT solvers. The stated goal is to reduce the volume of conditions that must be proved manually, thereby making deductive verification feasible for industrial systems comprising hundreds or thousands of processes.

Significance. If the proposed techniques can be shown to preserve soundness while automating a non-trivial fraction of verification conditions, the work would address a recognized scalability barrier in the deductive verification of process-oriented control software. The paper correctly identifies the practical problem and situates the proposal relative to prior VC-generation work for Reflex; however, the draft supplies neither a prototype, a worked example, nor any measurement of VC reduction, so the claimed practical benefit remains unassessed.

major comments (2)
  1. [Abstract] Abstract: the central claim that the three modifications 'will automate the proof of some of these conditions' is asserted without any concrete example, derivation, or preliminary data. A minimal worked example on a small Reflex program, showing which VCs become automatically solvable, is required to substantiate the claim.
  2. [Proposed modifications (invariant generation)] Description of invariant generation: the manuscript does not specify the syntactic form of the generated invariants, the algorithm that produces them from program structure, or any argument that the invariants are sound with respect to the original Reflex semantics. This omission directly affects whether the proposed automation preserves the correctness of the verification pipeline.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. We agree that the current draft is preliminary and lacks the concrete details and examples needed to substantiate the proposed automation. The revised manuscript will incorporate a minimal worked example and a full specification of the invariant generation technique, including its syntactic form, generation algorithm, and soundness argument.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that the three modifications 'will automate the proof of some of these conditions' is asserted without any concrete example, derivation, or preliminary data. A minimal worked example on a small Reflex program, showing which VCs become automatically solvable, is required to substantiate the claim.

    Authors: We agree that the abstract claim requires substantiation. The manuscript is a high-level proposal for modifications to the existing VC generator. In the revision we will add a minimal worked example based on a small Reflex program. The example will show the original VCs, the effect of the annotation language and generated invariants, and which conditions become solvable by the SMT solver. revision: yes

  2. Referee: [Proposed modifications (invariant generation)] Description of invariant generation: the manuscript does not specify the syntactic form of the generated invariants, the algorithm that produces them from program structure, or any argument that the invariants are sound with respect to the original Reflex semantics. This omission directly affects whether the proposed automation preserves the correctness of the verification pipeline.

    Authors: We acknowledge the omission. The draft focuses on the high-level idea of structure-derived invariants. In the revised version we will define the syntactic form of these invariants, present the algorithm that extracts them from Reflex program structure (process states and transitions), and supply a soundness argument showing that the generated invariants are implied by the original Reflex operational semantics. revision: yes

Circularity Check

0 steps flagged

High-level design proposal with no derivation, equations, or self-referential reductions

full rationale

The manuscript is a forward-looking proposal for tool modifications (annotation language, structure-based invariants, SMT pre-solving) to an existing VCG. It contains no equations, no fitted parameters, no predictions, and no derivation chain that could reduce to its inputs. The single self-citation to the authors' prior VCG work merely identifies the baseline problem (too many VCs) and is not used to justify any uniqueness theorem or load-bearing claim inside the present paper. All other patterns (self-definitional, fitted-input-as-prediction, ansatz smuggling, renaming) are absent by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The document is a tool-proposal paper rather than a mathematical derivation; it introduces no free parameters, mathematical axioms, or new postulated entities.

pith-pipeline@v0.9.1-grok · 5721 in / 988 out tokens · 19674 ms · 2026-06-26T06:36:04.740398+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

21 extracted references · 6 canonical work pages

  1. [1]

    Hyper-automaton: a model of control algorithms,

    V . E. Zyubin, “Hyper-automaton: a model of control algorithms,” in 2007 Siberian Conference on Control and Communications, 2007, pp. 51–57. [Online]. Available: https://doi.org/10.1109/SIBCON.2007. 371297

    work page doi:10.1109/sibcon.2007 2007

  2. [2]

    Reflex language: a practical notation for cyber-physical systems,

    V . E. Zyubin, T. V . Liakh, and A. S. Rozov, “Reflex language: a practical notation for cyber-physical systems,”System Informatics, no. 12, pp. 85–104, 2018. [Online]. Available: https://doi.org/10.31144/si.2307-6410.2018.n12.p85-104

    work page doi:10.31144/si.2307-6410.2018.n12.p85-104 2018

  3. [3]

    Reflex translator,

    A. Bastrykina, “Reflex translator,” https://github.com/a-bastrykina/ reflex-translator-diploma, 2020

    2020

  4. [4]

    doi:10.1007/978-3-319-91908-9\ 23

    R. H ¨ahnle and M. Huisman, “Deductive software verification: from pen-and-paper proofs to industrial tools,”Computing and Software Science: State of the Art and Perspectives, pp. 345–373, 2019. [Online]. Available: https://doi.org/10.1007/978-3-319-91908-9 18

    work page doi:10.1007/978-3-319-91908-9 2019

  5. [5]

    Hoare logic for java in isabelle/hol,

    D. von Oheimb, “Hoare logic for java in isabelle/hol,”Concurrency and Computation: Practice and Experience, vol. 13, no. 13, pp. 1173– 1214, 2001. [Online]. Available: https://doi.org/10.1002/cpe.598

    work page doi:10.1002/cpe.598 2001

  6. [6]

    A verification environment for sequential imperative programs in isabelle/hol,

    N. Schirmer, “A verification environment for sequential imperative programs in isabelle/hol,” inLogic for Programming, Artificial Intelligence, and Reasoning, F. Baader and A. V oronkov, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 398–414. [Online]. Available: https://doi.org/10.1007/b106931

    work page doi:10.1007/b106931 2005

  7. [7]

    An operational and axiomatic semantics for non- determinism and sequence points in c,

    R. Krebbers, “An operational and axiomatic semantics for non- determinism and sequence points in c,” vol. 49, no. 1, p. 101–112, Jan

  8. [8]

    Available: https://doi.org/10.1145/2578855.2535878

    [Online]. Available: https://doi.org/10.1145/2578855.2535878

    work page doi:10.1145/2578855.2535878

  9. [9]

    Verification condition generator for revised reflex language using isabelle/hol,

    A. D. Ishchenko and I. S. Anureev, “Verification condition generator for revised reflex language using isabelle/hol,” in2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM). IEEE, 2025, pp. 1440–1445

    2025

  10. [10]

    Parr,The Definitive ANTLR 4 Reference, 2nd ed

    T. Parr,The Definitive ANTLR 4 Reference, 2nd ed. Pragmatic Bookshelf, 2013. [Online]. Available: http://digital.casalini.it/ 9781680505016

    2013

  11. [11]

    Reflex grammar,

    A. Ishchenko, “Reflex grammar,” https://github.com/bearhug15/ ReflexVCG/blob/master/src/main/java/su/nsk/iae/reflex/antlr/ NewReflex.g4, 2024

    2024

  12. [12]

    Jml: A notation for detailed design,

    G. T. Leavens, A. L. Baker, and C. Ruby, “Jml: A notation for detailed design,” pp. 175–188, 1999

    1999

  13. [13]

    Acsl: Ansi/iso c specification,

    P. Baudin, J.-C. Filli ˆatre, C. March ´e, B. Monate, Y . Moy, and V . Prevosto, “Acsl: Ansi/iso c specification,” 2021

    2021

  14. [14]

    Two-step deductive verification of control software using reflex,

    I. Anureev, N. Garanina, T. Liakh, A. Rozov, V . Zyubin, and S. Gorlatch, “Two-step deductive verification of control software using reflex,” inInternational Andrei Ershov Memorial Conference on Perspectives of System Informatics. Springer, 2019, pp. 50–63

    2019

  15. [15]

    Satisfiability modulo theories,

    C. Barrett and C. Tinelli, “Satisfiability modulo theories,” pp. 305– 343, 2018

    2018

  16. [16]

    Solving sat and sat modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll (t),

    R. Nieuwenhuis, A. Oliveras, and C. Tinelli, “Solving sat and sat modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll (t),”Journal of the ACM (JACM), vol. 53, no. 6, pp. 937–977, 2006

    2006

  17. [17]

    Quantifier instantiation techniques for finite model finding in smt,

    A. Reynolds, C. Tinelli, A. Goel, S. Krsti ´c, M. Deters, and C. Barrett, “Quantifier instantiation techniques for finite model finding in smt,” pp. 377–391, 2013

    2013

  18. [18]

    The smt-lib standard: Version 2.0,

    C. Barrett, A. Stump, C. Tinelliet al., “The smt-lib standard: Version 2.0,” vol. 13, p. 14, 2010

    2010

  19. [19]

    Z3: An efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337–340

    2008

  20. [20]

    Barrett, C

    C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi ´c, T. King, A. Reynolds, and C. Tinelli, “cvc4,” inInternational Conference on Computer Aided Verification. Springer, 2011, pp. 171–177

    2011

  21. [21]

    cvc5: A versatile and industrial-strength smt solver,

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzliet al., “cvc5: A versatile and industrial-strength smt solver,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2022, pp. 415–442

    2022