arxiv: 2605.04377 · v1 · submitted 2026-05-06 · 💻 cs.PL

Recognition: unknown

Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types

Jean-Baptiste Jeannin, Jiawei Chen, Marc Pouzet, Serra Z. Dane

Authors on Pith no claims yet

Pith reviewed 2026-05-08 16:58 UTC · model grok-4.3

classification 💻 cs.PL

keywords formal verificationhybrid systemssynchronous languagesrefinement typesoperational semanticszero crossingsinitial value problemstype soundness

0 comments

The pith

Refinement types extended with hybrid semantics enable sound verification of synchronous programs with continuous dynamics.

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

This paper develops a way to formally verify safety-critical hybrid systems directly in their executable synchronous code. It defines precise rules for how the language handles solving differential equations as initial value problems and detecting zero crossings to trigger discrete events. The type system is then extended using refinement types to specify and check properties like avoiding unsafe states during continuous evolution. Soundness is proven, meaning any program passing the type checker will behave as specified. This matters for systems like autonomous vehicles where both modeling and implementation need to be trustworthy.

Core claim

We formalize the operational semantics of initial value problems and zero-crossing detection in a synchronous programming language, extend its refinement type system to support verification of these hybrid features, and prove that the extended type system is sound with respect to the semantics.

What carries the argument

The refinement type system extended to handle hybrid behaviors, which uses the formalized operational semantics to ensure that typed programs satisfy their safety specifications during both discrete and continuous phases.

If this is right

Hybrid programs can be both executed and verified in the same language without needing separate abstract models.
Safety properties involving continuous dynamics, such as avoiding certain thresholds, can be statically checked.
The soundness proof provides a rigorous guarantee that verified programs will not violate their specifications.
This approach applies to a wider variety of cyber-physical system controllers that include differential equations.

Where Pith is reading between the lines

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

Integrating this verification into compilers could allow automatic checking of control code for robots and aircraft.
The method might extend to other hybrid features like mode switches or stochastic elements in future developments.
Comparing this semantics to standard hybrid automata could reveal equivalences or differences in expressiveness.

Load-bearing premise

The operational semantics for initial value problems and zero-crossing detection provide an accurate model of real-world continuous physical behavior that the type system can rely on for soundness.

What would settle it

A counterexample program that satisfies the refinement types but produces an execution trace violating a specified safety property during continuous evolution, or a mismatch between the formalized zero-crossing detection and actual numerical solvers in a test case.

Figures

Figures reproduced from arXiv: 2605.04377 by Jean-Baptiste Jeannin, Jiawei Chen, Marc Pouzet, Serra Z. Dane.

**Figure 1.** Figure 1: Visualization of the 85 different cases studied in this paper: Rows A–G represent the seven possible behaviors of f on arbitrarily small left neighborhoods of a, and columns 1–7 represent the symmetric seven behaviors on arbitrarily small right neighborhoods of b. Each panel shows the function shape corresponding to the intersection of the row and column cases. For each case (e.g. E4), there are two subc… view at source ↗

**Figure 2.** Figure 2: Program Syntax The central hybrid construct is let rec der . . . init . . . reset . . . in ce, which describes a continuous segment governed by an ODE together with event triggered resets that restart the segment when an upward zero-crossing is detected. Tuples provide a uniform way to represent multi-dimensional continuous state, which is needed because many of our examples evolve over several continuous… view at source ↗

**Figure 3.** Figure 3: Hybrid Type Syntax 5.1 Water Tank A hybrid system often has multiple reset conditions and these resets do not always have direct influence over the variable of interest. The following program demonstrates a controller which is responsible for filling or draining a tank of water to maintain its level between two setpoints. In this case, the resets do not directly set the water level but instead influence it… view at source ↗

**Figure 4.** Figure 4: Hybrid Stream Semantics of the form S; σ ⊢ e (v(t),tr);[vr|nil] ,→ e ′ zero. The semantics of Zélus deterministically chooses the first zero-crossing by syntactic order. Finally, when a zero-crossing is encountered, the j-th expression representing its reset is evaluated with the values of the continuous variables immediately prior to reset populated in its context. (S-LETREC-DER-INF) has a similar structu… view at source ↗

**Figure 5.** Figure 5: Stream Typing Rules for Hybrid Expressions safety predicate may be designated by the user as the part to be established by differential reasoning. In this way, the existential form of the rule reflects proof flexibility for the metatheory, while still admitting a practical implementation. Finally, all possible resets of the system are proven safe with respect to their triggering conditions to ensure that t… view at source ↗

**Figure 1.** Figure 1: In examples of this section, when a function is undefined at a point, view at source ↗

read the original abstract

Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of certainty. Formal verification has been employed to verify the software controlling these systems, but due to their complexity, is usually performed on an abstract model rather than the executable code. Synchronous programming languages extended with differential equations promise both rigorous modeling and sufficient expressiveness to implement executable controller code, and recent developments have introduced formal verification of strictly discrete-time programs. Extending these verification techniques to hybrid systems enables precise modeling of the environment for a wider variety of programs to be both verified and executed. We formalize the operational semantics of initial value problems and zero-crossing detection expressed in a synchronous programming language, extend its type system for verification thereof, and prove its soundness.

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.

Desk Editor's Note private letter to a colleague

This paper formalizes hybrid operational semantics for synchronous programs including IVPs and zero-crossings, adds refinement types for verification, and claims a soundness proof, but the details of that proof are what matter most.

read the letter

The core advance here is taking prior work on verifying discrete synchronous programs with refinement types and extending the operational semantics and type system to cover hybrid features like differential equations and zero-crossing detection. They formalize how these are expressed in the language, adapt the types for safety properties, and state that they have proved the whole thing sound against an external mathematical semantics. That combination is new and directly targets the gap between verified models and executable controller code in CPS applications. If the formalization holds up, it lets people write and verify code that actually runs on the target system rather than just an abstraction of it. The approach looks clean on the surface for handling the discrete-continuous boundary in a synchronous setting. The main soft spot is the soundness proof itself. The abstract asserts it exists, but without the lemmas, the handling of edge cases like simultaneous zero-crossings or accumulation points, or the precise definition of the continuous semantics, it is impossible to tell whether the proof is tight or leaves gaps. Hybrid semantics are notoriously tricky, and any mismatch between the chosen operational rules and real continuous behavior would undermine the verification guarantees. The paper does not appear to introduce circular reasoning or rely on invented entities, which is good. This is for people working in programming languages for cyber-physical systems who already know synchronous languages and refinement types. A reader in that niche would find the extension useful to see, even if they end up adapting parts of it. It is worth sending to peer review because the claim is a non-trivial formal result in an area where soundness matters for safety-critical use. Reviewers will need to check the proof carefully, but the work is grounded enough to justify the time.

Referee Report

1 major / 1 minor

Summary. The manuscript formalizes the operational semantics of initial value problems (IVPs) and zero-crossing detection within a synchronous programming language for hybrid systems. It extends the language's type system with refinement types to support verification of safety properties and includes a proof of soundness for the resulting verification framework.

Significance. If the soundness proof is complete and the chosen hybrid semantics are faithful, the work would be significant for enabling direct formal verification of executable controller code in cyber-physical systems rather than relying solely on separate abstract models. This approach could improve precision and reduce modeling gaps in safety-critical domains such as autonomous vehicles and robotics, while the use of refinement types offers a practical mechanism for expressing and checking continuous-discrete properties.

major comments (1)

[Abstract / soundness proof] Abstract and soundness section: the claim of a soundness proof is central, yet the provided description does not detail the lemmas, induction strategy, or explicit treatment of edge cases in the hybrid semantics (e.g., non-unique IVP solutions or chattering zero-crossings). Without these, gaps in the proof cannot be ruled out and the central claim remains difficult to verify.

minor comments (1)

[Introduction / semantics section] The weakest assumption noted (modeling fidelity of IVPs and zero-crossings) is an external-validity concern rather than an internal inconsistency; if the paper intends to address it, a brief discussion of the chosen mathematical semantics versus real-world approximations would strengthen the presentation.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for highlighting the need for greater clarity in the presentation of the soundness proof. We address the major comment below.

read point-by-point responses

Referee: [Abstract / soundness proof] Abstract and soundness section: the claim of a soundness proof is central, yet the provided description does not detail the lemmas, induction strategy, or explicit treatment of edge cases in the hybrid semantics (e.g., non-unique IVP solutions or chattering zero-crossings). Without these, gaps in the proof cannot be ruled out and the central claim remains difficult to verify.

Authors: We agree that the abstract is high-level by design and that the soundness section would benefit from additional exposition to facilitate verification of the proof. We will revise the manuscript to include an explicit outline of the lemmas, the induction strategy (by induction over derivation length in the operational semantics), and dedicated discussion of the cited edge cases. In particular, we will state the Lipschitz conditions under which IVP uniqueness holds in our semantics and add a lemma establishing that the zero-crossing detection rule precludes chattering. These additions will be placed in the soundness section without altering the underlying formalization. revision: yes

Circularity Check

0 steps flagged

No significant circularity in formal semantics and soundness proof

full rationale

The paper defines operational semantics for initial value problems and zero-crossings, extends a refinement type system, and proves soundness. This follows the standard structure of formal methods work: semantics are introduced as a mathematical model, the type system is defined relative to it, and soundness is established by induction or similar proof techniques. No load-bearing step reduces by construction to a fitted parameter, self-citation chain, or renamed input; the derivation is self-contained against the external mathematical semantics of hybrid systems rather than being tautological.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Relies on standard mathematical definitions of differential equations and initial value problems plus domain assumptions about zero-crossing behavior in synchronous languages; no free parameters or invented entities are introduced.

axioms (2)

standard math Operational semantics of initial value problems for differential equations
Invoked when formalizing hybrid program execution.
domain assumption Zero-crossing detection semantics in synchronous languages
Core to the hybrid extension being verified.

pith-pipeline@v0.9.0 · 5441 in / 1186 out tokens · 21802 ms · 2026-05-08T16:58:57.559730+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

34 extracted references · 26 canonical work pages

[1]

In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H

Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: An al- gorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lec- ture Notes in Computer Science, vol. 736, pp. 209–229. Springer (1993).https: //doi.org/10.1007/3-540-57318-6_30

work page doi:10.1007/3-540-57318-6_30 1993
[2]

Specification-

Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Ničković, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Lectures on Runtime Verification: Introductory and Advanced Topics, pp. 135–175. Springer (2018).https://doi. org/10.1007/978-3-319-75632-5_5

work page doi:10.1007/978-3-319-75632-5_5 2018
[3]

Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybridsystemsmodelers.JournalofComputerandSystemSciences78(3),877–910 (2012).https://doi.org/10.1016/j.jcss.2011.08.009

work page doi:10.1016/j.jcss.2011.08.009 2012
[4]

Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybridsystemsmodelers.JournalofComputerandSystemSciences78(3),877–910 (2012)

2012
[5]

In: Proceedings of the ninth ACM international conference on Embedded software - EMSOFT ’11

Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: A hybrid synchronous lan- guage with hierarchical automata: static typing and translation to synchronous code. In: Proceedings of the ninth ACM international conference on Embedded software - EMSOFT ’11. p. 137. ACM Press, Taipei, Taiwan (2011).https: //doi.org/10.1145/2038642.2038664

work page doi:10.1145/2038642.2038664 2011
[6]

Proceedings of the IEEE 91(1), 64–83 (2003).https://doi.org/10.1109/JPROC.2002.805826

Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., De Si- mone, R.: The synchronous languages twelve years later. Proceedings of the IEEE 91(1), 64–83 (2003).https://doi.org/10.1109/JPROC.2002.805826

work page doi:10.1109/jproc.2002.805826 2003
[7]

In: Ritter, G

Berry, G.: Real time programming: Special purpose or general purpose languages. In: Ritter, G. (ed.) Information Processing ’89: Proceedings of the IFIP 11th World Computer Congress. pp. 11–17. Elsevier Science Publishers B.V. (North-Holland) (1989)

1989
[8]

Science of Computer Programming19(2), 87–152 (1992).https://doi.org/10.1016/0167-6423(92)90005-V

Berry, G., Gonthier, G.: The Esterel synchronous programming language: De- sign, semantics, implementation. Science of Computer Programming19(2), 87–152 (1992).https://doi.org/10.1016/0167-6423(92)90005-V

work page doi:10.1016/0167-6423(92)90005-v 1992
[9]

Bourke,T.,Pouzet,M.:Zélus:AsynchronouslanguagewithODEs.In:Proceedings of the 16th international conference on Hybrid systems: computation and control. pp. 113–118 (2013).https://doi.org/10.1145/2461328.2461348

work page doi:10.1145/2461328.2461348 2013
[10]

In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. pp. 178–188 (1987).https: //doi.org/10.1145/41625.41641

work page doi:10.1145/41625.41641 1987
[11]

Springer (1991).https://doi.org/ 10.1007/978-1-4757-3922-0

Cellier, F.E.: Continuous System Modeling. Springer (1991).https://doi.org/ 10.1007/978-1-4757-3922-0

work page doi:10.1007/978-1-4757-3922-0 1991
[12]

Chen, J., de Mendonça, J.L.V., Ayele, B.S., Bekele, B.N., Jalili, S., Sharma, P., Wohlfeil, N., Zhang, Y., Jeannin, J.B.: Synchronous Programming with Refinement Types8(ICFP), 268:938–268:972 (Aug 2024).https://doi.org/10.1145/3674657

work page doi:10.1145/3674657 2024
[13]

In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)

Colaço, J.L., Pagano, B., Pouzet, M.: Scade 6: A formal language for embedded critical software development (invited paper). In: 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE). pp. 1–11. IEEE (2017). https://doi.org/10.1109/TASE.2017.8285623 22 Dane et al

work page doi:10.1109/tase.2017.8285623 2017
[14]

In: International Conference on Automated Deduction

Fulton, N., Mitsch, S., Quesel, J.D., Völp, M., Platzer, A.: Keymaera X: An ax- iomatic tactical theorem prover for hybrid systems. In: International Conference on Automated Deduction. pp. 527–538. Springer (2015).https://doi.org/10.1007/ 978-3-319-21401-6_36

2015
[15]

In: Proceedings 11th Annual IEEESymposiumonLogicinComputerScience(LICS).pp.278–292.IEEE(1996)

Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Annual IEEESymposiumonLogicinComputerScience(LICS).pp.278–292.IEEE(1996). https://doi.org/10.1109/LICS.1996.561342

work page doi:10.1109/lics.1996.561342 1996
[16]

Jhala, R., Vazou, N.: Refinement types: A tutorial. Found. Trends Program. Lang. 6(3–4), 159–317 (Oct 2021).https://doi.org/10.1561/2500000032

work page doi:10.1561/2500000032 2021
[17]

Leibniz Transactions on Embedded Systems8(2), 04–1 (2022)

Kamburjan, E., Mitsch, S., Hähnle, R.: A hybrid programming language for formal modeling and verification of hybrid systems. Leibniz Transactions on Embedded Systems8(2), 04–1 (2022)

2022
[18]

Pattern Recog- nition153, 110500 (2024).https://doi.org/https://doi.org/10.1016/j

Konečný, M., Taha, W., Bartha, F., Duracz, J., Duracz, A., Ames, A.: Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point. Nonlinear Analysis: Hybrid Systems20, 1–20 (May 2016).https://doi.org/10.1016/j. nahs.2015.10.004

work page doi:10.1016/j 2016
[19]

Proceedings of the IEEE79(9), 1321–1336 (Sep 1991)

Le Guernic, P., Gautier, T., Le Borgne, M., Le Maire, C.: Programming real-time applications with SIGNAL. Proceedings of the IEEE79(9), 1321–1336 (Sep 1991). https://doi.org/10.1109/5.97301

work page doi:10.1109/5.97301 1991
[20]

In: Hybrid Sys- tems: Computation and Control (HSCC 2005)

Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Hybrid Sys- tems: Computation and Control (HSCC 2005). Lecture Notes in Computer Science, vol. 3414, pp. 25–53 (2005).https://doi.org/10.1007/978-3-540-31954-2_2

work page doi:10.1007/978-3-540-31954-2_2 2005
[21]

ACM Trans- actions on Embedded Computing Systems22(5s), 155:1–155:24 (2023).https: //doi.org/10.1145/3609134

Lin, S., Manerkar, Y.A., Lohstroh, M., Polgreen, E., Yu, S.J., Jerad, C., Lee, E.A., Seshia, S.A.: Towards building verifiable CPS using lingua franca. ACM Trans- actions on Embedded Computing Systems22(5s), 155:1–155:24 (2023).https: //doi.org/10.1145/3609134

work page doi:10.1145/3609134 2023
[22]

In: Butler, M., Schulte, W

Loos, S.M., Platzer, A., Nistor, L.: Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In: Butler, M., Schulte, W. (eds.) FM 2011: For- mal Methods, vol. 6664, pp. 42–56. Springer Berlin Heidelberg, Berlin, Heidel- berg (2011).https://doi.org/10.1007/978-3-642-21437-0_6, series Title: Lec- ture Notes in Computer Science

work page doi:10.1007/978-3-642-21437-0_6 2011
[23]

Marin, M., Ölveczky, P.C., Reja, M., Rukhaia, M., Bae, K., Dundua, B.: Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic. Tech. rep., University of Oslo / collaborators (technical report) (2024)

2024
[24]

Journal of Functional Programming18(5-6), 865–911 (2008).https: //doi.org/10.1017/S0956796808006953

Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. Journal of Functional Programming18(5-6), 865–911 (2008).https: //doi.org/10.1017/S0956796808006953

work page doi:10.1017/s0956796808006953 2008
[25]

Journal of Automated Reasoning41(2), 143–189 (2008).https://doi.org/10.1007/ s10817-008-9103-8

Platzer, A.: Differential dynamic logic for hybrid systems. Journal of Automated Reasoning41(2), 143–189 (2008).https://doi.org/10.1007/ s10817-008-9103-8

2008
[26]

Springer International Publishing, Cham (2018).https://doi.org/10.1007/978-3-319-63588-0

Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer International Publishing, Cham (2018).https://doi.org/10.1007/978-3-319-63588-0

work page doi:10.1007/978-3-319-63588-0 2018
[27]

A Complete Uniform Substitution Calculus for Differential Dynamic Logic

Platzer, A.: A Complete Uniform Substitution Calculus for Differential Dynamic Logic. Journal of Automated Reasoning59(2), 219–265 (Aug 2017).https://doi. org/10.1007/s10817-016-9385-1

work page doi:10.1007/s10817-016-9385-1 2017
[28]

Prajna, S., Jadbabaie, A.: Safety Verification of Hybrid Systems Using Barrier Certificates. pp. 477–492. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2004).https://doi.org/10.1007/978-3-540-24743-2_32

work page doi:10.1007/978-3-540-24743-2_32 2004
[29]

In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementa- tion

Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementa- tion. pp. 159–169 (2008).https://doi.org/10.1145/1375581.1375602 Towards Formal Verification of Hybrid Synchronous Programs 23

work page doi:10.1145/1375581.1375602 2008
[30]

In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell

Vazou, N., Seidel, E.L., Jhala, R.: Liquid Haskell: Experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell. pp. 39–51 (2014).https://doi.org/10.1145/2633357.2633366

work page doi:10.1145/2633357.2633366 2014
[31]

In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

White, L., Titolo, L., Slagel, J.T., Muñoz, C.: A temporal differential dynamic logic formal embedding. In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 162–176. CPP 2024, Association for Computing Machinery, New York, NY, USA (2024).https://doi.org/10. 1145/3636501.3636943

work page arXiv 2024
[32]

Information and Computation115(1), 38–94 (1994).https://doi.org/10.1006/inco.1994

Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation115(1), 38–94 (1994).https://doi.org/10.1006/inco.1994. 1093 24 Dane et al. A Case Distinction We have identified the following 7 cases forx < a: Afis strictly negative in a ball left ofa. Formally:ℓ < aand∃η >0,∀x∈ [a−η, a), f(x)<0. Examples:(x−a) 2k+1,−|x−a| ...

work page doi:10.1006/inco.1994 1994
[33]

there exists an indexjwhose guard triggers attr (first upward zero-crossing),
[34]

decreasing sawtooth

and the reset branch steps in the discrete fragment under the post-flow store S;σ,[x7→ρ(t r)(x) ::nil], producing a rewritten reset expressionde ′ r,j, and the equation residuale ′ is obtained by replacing the initial value with the post-reset state and the reset branch tode′ r,j, wherev r,j is emitted. (1) Safety of the finite continuous trajectory.T-DER...