Pith. sign in

REVIEW 4 major objections 6 minor 26 references

StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

T0 review · 4 major / 6 minor · reviewed 2026-08-02 · deepseek-v4-flash

Pith's one-line read An open-source toolbox synthesizes stochastic barrier functions orders of magnitude faster than existing tools, with tighter safety bounds and support for higher-dimensional systems.

desk verdict A useful SBF synthesis toolbox whose headline performance claims are plausible, but the PWC guarantees rest on unverified transition-kernel bound computations. read the letter →

arxiv 2602.20359 v3 pith:2BD6TJPL submitted 2026-02-23 eess.SY cs.SYmath.OC

classification eess.SYcs.SYmath.OC
keywords stochasticbarrierfunctionsprobabilisticsafetyformalverificationsum-of-squaresoptimizationpiecewise-constantlinearprogramminggradientdescentconvex
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

StochasticBarrier.jl is an open-source toolbox that automatically constructs stochastic barrier functions—certificates giving a formal lower bound on the probability that a system with additive Gaussian noise stays within a safe set over a finite horizon. The paper's central claim is that this toolbox outperforms the previously available SBF-synthesis tools on all three relevant axes: computation time (up to four orders of magnitude faster), tightness of the resulting safety-probability bound (turning trivial 0 guarantees into non-trivial ones), and scalability (handling systems with twice the dimensionality that competitors can manage). This is achieved by combining sum-of-squares optimization for polynomial systems with piecewise-constant barrier methods based on linear programming and gradient descent, including support for piecewise-affine-bounded dynamics so that non-polynomial systems become verifiable. A reader should care because formal safety verification of stochastic systems is a bottleneck in deploying learning-based controllers in robotics and autonomy, and a fast, general tool turns SBF synthesis from a research exercise into a practical engineering step.

What carries the argument

A stochastic barrier function (SBF) is a nonnegative function B satisfying three conditions: B(x) >= 1 outside the safe set, B(x) <= eta on the initial set, and E[B(f(x)+w)] <= B(x) + beta inside the safe set; these conditions guarantee safety probability P_s >= 1 - (eta + N*beta). The toolbox computes such a B via two routes: (i) sum-of-squares (SOS) optimization, where B is a polynomial and the conditions are enforced through semidefinite programming (Theorems 2.1 and 2.2); and (ii) piecewise-constant (PWC) synthesis, where the state space is partitioned into hyperrectangles, lower and upper bounds on the transition kernel between cells are computed (Eq. 7), and the cell values b_i are fou

What would settle it

For a simple 1D linear system with Gaussian noise, compute the exact transition probability from each grid cell to every other cell using numerical quadrature, and compare with the toolbox's reported lower and upper bounds; any violation invalidates the piecewise-constant safety guarantee.

Watch

Extended reading notes

Core claim

The paper presents StochasticBarrier.jl, a toolbox for synthesizing stochastic barrier functions for discrete-time stochastic systems with additive Gaussian noise. It implements two families of synthesis methods: sum-of-squares optimization for linear, polynomial, and piecewise-affine-bounded dynamics, and piecewise-constant barrier synthesis via dual linear programming, counterexample-guided inductive synthesis, and projected gradient descent. The central claim is empirical: across more than 30 benchmarks spanning systems of dimension one to six, the toolbox reports beating the two existing SBF-synthesis tools in computation time by up to four orders of magnitude, producing safety-probabili

Load-bearing premise

The piecewise-constant safety certificates rest entirely on the correctness of the computed lower and upper bounds on the transition kernel over each grid cell; if those bounds are not rigorous, the reported safety probability can be overestimated.

Editorial extensions

If this is right

  • SBF synthesis becomes practical for higher-dimensional systems (up to six dimensions demonstrated) and for high-degree polynomial barriers, where prior tools ran out of memory or failed.
  • Piecewise-constant synthesis provides non-trivial safety guarantees for non-polynomial systems such as a hybrid unicycle, where sum-of-squares methods return only a trivial safety probability of 0.
  • Users can choose among engines: dual LP and CEGIS give the tightest probability bounds, while gradient descent scales to large partition counts while still returning sound (though not globally optimal) eta/beta values.
  • The ability to save and load precomputed transition bounds lets users amortize the cost of probability computation across repeated safety analyses.
  • If the reported speedups reproduce on other hardware, SBF-based verification can be embedded in interactive design loops or online monitoring for autonomous systems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • In our reading, the soundness of the piecewise-constant certificates hinges on the transition kernel bound computation, which the paper does not independently verify; a formal proof or high-precision check of those bounds would close the main gap.
  • The benchmark comparisons inherit differences in problem formulation across tools (for instance, how the safety probability is defined), so the reported margins may not hold on every problem instance; a neutral reimplementation would quantify that.
  • The piecewise-constant machinery is, in principle, agnostic to the noise distribution, suggesting a natural extension beyond Gaussian additive noise to data-driven or non-Gaussian settings.
  • The modular design—separate transition-bound computation and barrier-synthesis engines—should make the toolbox a convenient substrate for future SBF research, such as control synthesis or falsification.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

Summary. The paper presents StochasticBarrier.jl, an open-source Julia toolbox for synthesizing stochastic barrier functions (SBFs) for discrete-time stochastic systems with additive Gaussian noise. The toolbox supports three classes of dynamics — linear, polynomial, and piecewise affine (PWA) inclusion — and three classes of barrier functions: SOS polynomials, piecewise constant (PWC) functions via dual linear programming, CEGIS, and gradient descent, and SOS for PWA inclusions. The authors benchmark against PRoTECT and StochasticBarrierFunctions across over 30 case studies, claiming orders-of-magnitude speedups, tighter safety probability bounds, and scalability to higher dimensions and higher-degree SOS barriers. The central claim is the engineering value of the toolbox rather than a new mathematical theorem; the theory is drawn from prior work [13, 14, 23].

Significance. If the claimed performance and correctness hold, StochasticBarrier.jl would be a valuable contribution: it is open-source, provides multiple synthesis engines, includes convenient NetCDF storage for transition probabilities, and appears to handle PWC barriers for nonlinear systems where SOS-based tools fail (e.g., the unicycle example in Fig. 2c). The paper explicitly positions itself as a toolbox paper, so the lack of new theorems is appropriate. However, the most load-bearing component — the computation of guaranteed interval bounds on the transition kernel in Eq. (7) — is not described, proved, or externally validated in this manuscript. The correctness of all PWC certificates, and hence the claimed safety-probability improvements, rests on this unverified step. The benchmark comparisons also contain unexplained numerical coincidences and lack variance information, which weakens the strength of the speed/scalability claims. These issues are fixable within the scope of a toolbox paper, but they must be addressed before the central claims can be accepted.

major comments (4)
  1. [§2.2.2 (Eq. 7) and §3.1.1] The PWC safety certificate in Theorem 2.3 depends on the values p_ij and p_ij_bar defined in Eq. (7) as exact infimum and supremum of the transition kernel over each partition cell. Section 3.1.1 states that transition_probabilities() computes these bounds, but no algorithm, numerical integration scheme, or error analysis is provided. For additive Gaussian noise and hyperrectangle partitions, the extrema of a Gaussian CDF over a box are not generally obtained by evaluating at corners; a naive sampling or interval-arithmetic implementation may fail to enclose the true range. If the bounds are not guaranteed, the LP/GD constraints in Theorem 2.3 are solved with invalid data, and the resulting P_s lower bound in Eq. (3) is not sound. This directly affects the headline advantages of the PWC engines, including the unicycle case where SOS returns zero. Please provide the precise algorithm used
  2. [Table 3 and Fig. 1] Several rows of Table 3 report numerically identical η, β, and P_s values for StochasticBarrier.jl and PRoTECT (e.g., Contraction Map 1 at degrees 2, 4, 8, 12: both give η=1.7e-2, β=1.8e-2, P_s=0.80; similar at degrees 24/30, and for Two Tank at degree 10/12). Given that PRoTECT is a separate Python implementation and the paper states its results are averaged over 10 random runs and that its P_s definition was adjusted, exact equality to the precision shown is implausible unless the two tools solve a mathematically identical program to machine precision. If the values are truly identical because the problem formulations coincide, state this explicitly; otherwise, the reported numbers may contain an error. This is load-bearing because the comparison is the evidence for the 'tightness of safety probability' claim. Please clarify the adjustment procedure for PRoTECT's P_s and provide the ac
  3. [§4 (Benchmark Studies) and §3.2.2] The runtime claims ('up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems') are based on single-run experiments, except for PRoTECT which is averaged over 10 runs. No confidence intervals, standard deviations, or multiple-seed results are reported for StochasticBarrier.jl's own methods, including the GD engine whose hyperparameters (initial_lr, decay, momentum, num_iterations) are user-specified and whose convergence is not guaranteed to a certified optimum. The comparison would be more convincing with repeated runs (at least for the GD and CEGIS methods) and a sensitivity analysis of the GD hyperparameters. Without this, the quantitative speedup factors in the abstract are not statistically supported.
  4. [§3.2.2 (Gradient Descent)] The text states that for the GD method, 'at termination, the values for η, β are guaranteed to be sound with respect to the returned barrier, although not absolutely optimal in the sense of Theorem 2.3.' This soundness claim is not proven here and is not obvious from the described minimax formulation: projected gradient descent converges to a stationary point under convexity, but the returned η and β must be verified to satisfy the safety constraints for the returned barrier over the continuous state space. Since the GD engine is one of the three PWC engines and is the fastest, the validity of its safety certificate is a load-bearing property. Please provide the verification step or a formal theorem (with proof or citation to a machine-checked proof) that the GD output constitutes a valid SBF.
minor comments (6)
  1. [References] Reference [15] (Data-Driven Permissible Safe Control) is listed with the same arXiv identifier (2404.16986) as reference [13] (Piecewise Stochastic Barrier Functions). This appears to be a citation error; please correct.
  2. [§3.1.3] The generation of PWA bounds using 'Linear Bound Propagation [29]' is mentioned but no details are given on how a user produces the NetCDF file. Since this is a required input for PWA systems, a brief description or a pointer to the associated script would improve usability.
  3. [Fig. 2] The legend ordering in some subfigures (e.g., (b) Pendulum) makes it hard to map colors to the PWC methods; consider using consistent line styles and adding markers or a table of values for clarity.
  4. [§4 and Appendix D] The sentence 'All methods use Mosek as the underlying SDP solver' is ambiguous for the LP-based PWC methods, which by default use HiGHS. Clarify that Mosek is used for SOS/SDP and HiGHS for LP.
  5. [Appendix B.1] In the 'Contraction Map 2' description, 'using the same distribution w ∼ N(0, 10^-2 I)' is unclear because the preceding contraction map also uses 10^-2. Specify whether the noise variance is identical or reduced.
  6. [Eq. (3)] The displayed lower bound after condition (2c) is not numbered in the text, yet later references to 'Eq. (3)' appear. Please add the equation number.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the toolbox's performance claims are empirical and benchmarked against external tools; the only notable dependency is unverified numerical bound computation, which is a soundness risk rather than a definitional circularity.

full rationale

The paper's central claims are engineering/empirical: it benchmarks StochasticBarrier.jl against the external tools PRoTECT [28] and StochasticBarrierFunctions [23], so the reported speedups and safety-probability improvements are measured against independent implementations, not derived from the paper's own assumptions. The theoretical backbone (SBF conditions Eq. (2)–(3), SOS reductions Theorem 2.1, and PWC optimization Theorem 2.3) is imported from published sources [23] and the authors' own prior work [13,14]; these citations are load-bearing for soundness but are not circular because the toolbox does not define the safety probability to be the optimization objective—it solves the stated feasibility conditions and reports the resulting bound. The most notable unverified dependency is in Section 3.1.1/Eq. (7): transition_probabilities() is said to compute infimum/supremum transition-kernel bounds, but no algorithm, proof, or external verification is provided. If those bounds are not rigorous, Theorem 2.3's certificates would be unsound; this is a correctness risk, not a circularity. No equation reduces to its own input, no fitted parameter is renamed as a prediction, and no uniqueness argument is imported from the authors' prior work. The self-citation cluster is real but does not force the benchmark conclusions.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The paper's novel contribution is an implementation; all mathematical certificates are imported from published earlier work, partly by the same authors. The benchmark conclusions depend on user-chosen discretizations and hyperparameters.

free parameters (3)
  • PWC grid half-width / partition count |Q| = Examples: 640, 225, 289, 361 (Contraction Map 2); 120/240/480 (Pendulum); 1250/1800 (Unicycle)
    Chosen per benchmark; determines tightness of transition bounds and safety probability; no automatic refinement criterion or error analysis given.
  • GD hyperparameters (initial_lr=1e-2, decay=0.9999, momentum=0.9, num_iterations=10000) = 1e-2, 0.9999, 0.9, 10000
    Defaults selected by authors; the GD speed claim may depend on them; no sensitivity study reported.
  • SOS barrier/lagrange degrees = barrier_degree 2-30; lagrange_degree=2
    Chosen per benchmark; strongly affects runtime and bound tightness; no rule for selection given.
assumptions (5)
  • standard math Theorem 2.1 (SOS-SBF for polynomial systems) from [23] is correct.
    Used as the foundation of the SOS engine; not proved in this paper, only cited.
  • domain assumption Theorem 2.2 (SOS-SBF for PWA inclusion dynamics) from [14] is correct.
    Self-cited prior work; no independent proof or machine-check in this paper; central to PWA SOS claims.
  • domain assumption Theorem 2.3 (PWC-SBF) from [13] is correct.
    Self-cited prior work; implementation depends on it; not externally validated in this paper.
  • domain assumption transition_probabilities() computes valid lower/upper bounds of the Gaussian transition kernel over each hyperrectangle (Eq. 7).
    No numerical method or proof is provided; PWC safety guarantees depend on these bounds.
  • domain assumption PWA inclusion bounds from Linear Bound Propagation [29] bound the true dynamics on each partition.
    The PWA benchmark cases load precomputed NetCDF bounds; correctness of these bounds is assumed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis." pith.science (2026). https://pith.science/paper/2BD6TJPL

@misc{pith2026260220359,
  author       = {Pith},
  title        = {Pith review of: StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2BD6TJPL}},
  note         = {Machine review of arXiv:2602.20359}
}
read the original abstract

We present StochasticBarrier.jl, an open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise. StochasticBarrier.jl certifies linear, polynomial, and piecewise affine (PWA) systems. The latter enables verification for a wide range of system dynamics, including general nonlinear types. The toolbox implements a Sum-of-Squares (SOS) optimization approach, as well as methods based on piecewise constant (PWC) functions. For SOS-based SBFs, StochasticBarrier.jl leverages semi-definite programming solvers, while for PWC SBFs, it offers three engines: two using linear programming (LP) and one based on gradient descent (GD). Benchmarking StochasticBarrier.jl against the state-of-the-art shows that the tool outperforms existing tools in computation time, safety probability bounds, and scalability across over 30 case studies. Compared to its closest competitor, StochasticBarrier.jl is up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems.

Figures

Figures reproduced from arXiv: 2602.20359 by the authors.

Figure 1
Figure 1. Polynomial systems benchmarking of StochasticBarrier.jl vs StochasticBarrierFunctions [23] and PRoTECT [28]. Plots depict optimization time 𝜏 (𝑠) and probability of safety 𝑃𝑠 . If data points are not plotted, it means the algorithm ran out of memory. t 50 100 150 200 250 300 350 400 10 0 10 2 10 4 (s) 50 100 150 200 250 300 350 400 |Q| 0.2 0.4 0.6 0.8 1 P s SOS PWC Dual LP PWC CEGIS PWC GD (a) Contraction Map 100 15… view at source ↗
Figure 2
Figure 2. Benchmark plots for the three PWC-SBF methods. For the pendulum and unicycle, the SOS results are also depicted [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Input-output overview of StochasticBarrier.jl [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

26 extracted references · 6 linked inside Pith

  1. [1]

    A., Cauchi, N., Delicaris, J., Hartmanns, A., Khaled, M., Lavaei, A., Pilch, C., Remke, A., Schupp, S., et al.Arch-comp20 category report: Stochastic models

    Abate, A., Blom, H. A., Cauchi, N., Delicaris, J., Hartmanns, A., Khaled, M., Lavaei, A., Pilch, C., Remke, A., Schupp, S., et al.Arch-comp20 category report: Stochastic models. InARCH(2020)

  2. [2]

    ApS, M.Mosek optimization toolbox for matlab.User’s Guide and Reference Manual, Version 4, 1 (2019)

  3. [3]

    P., and Shreve, S

    Bertsekas, D. P., and Shreve, S. E.Stochastic Optimal Control: the Discrete-time Case, vol. 5. Athena Scientific, 2004

  4. [4]

    InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control(2019), pp

    Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., and Schilling, C.Ju- liareach: a toolbox for set-based reachability. InProceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control(2019), pp. 39–44

  5. [5]

    Coleman, C., Lyon, S., Maliar, L., and Maliar, S.Matlab, python, julia: What to choose in economics?Computational Economics 58(2021), 1263–1288

  6. [6]

    Forets, M., and Schilling, C.LazySets.jl: Scalable Symbolic-Numeric Set Computations.Proceedings of the JuliaCon Conferences 1, 1 (2021), 11

  7. [7]

    J.Parallelizing the dual revised simplex method

    Huangfu, Q., and Hall, J. J.Parallelizing the dual revised simplex method. Mathematical Programming Computation 10, 1 (2018), 119–142

  8. [8]

    [9]Legat, B.Multivariate polynomials in Julia

    Jagtap, P., Soudjani, S., and Zamani, M.Formal synthesis of stochastic systems via control barrier certificates.IEEE Transactions on Automatic Control 66, 7 (2020), 3097–3110. [9]Legat, B.Multivariate polynomials in Julia. InJuliaCon(July 2022)

Show all 26 references
  1. [10]

    P.JuMP 1.0: Recent improvements to a modeling language for mathematical optimization.Mathematical Programming Computation(2023)

    Lubin, M., Dowson, O., Dias Garcia, J., Huchette, J., Legat, B., and Vielma, J. P.JuMP 1.0: Recent improvements to a modeling language for mathematical optimization.Mathematical Programming Computation(2023)

  2. [11]

    B., Lahijanian, M., and Laurenti, L.IntervalMDP

    Mathiesen, F. B., Lahijanian, M., and Laurenti, L.IntervalMDP. jl: Accel- erated Value Iteration for Interval Markov Decision Processes.arXiv preprint arXiv:2401.04068(2024)

  3. [12]

    B., Romao, L., Calvert, S

    Mathiesen, F. B., Romao, L., Calvert, S. C., Laurenti, L., and Abate, A.A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution.arXiv preprint arXiv:2410.06662(2024)

  4. [14]

    Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions.Advances in Neural Information Processing Systems(2022)

    Mazouz, R., Muvvala, K., Ratheesh, A., Laurenti, L., and Lahijanian, M. Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions.Advances in Neural Information Processing Systems(2022)

  5. [15]

    B., Frew, E., Laurenti, L., and Lahija- nian, M.Data-Driven Permissible Safe Control with Barrier Certificates.arXiv preprint arXiv:2404.16986(2024)

    Mazouz, R., Skovbekk, J., Mathiesen, F. B., Frew, E., Laurenti, L., and Lahija- nian, M.Data-Driven Permissible Safe Control with Barrier Certificates.arXiv preprint arXiv:2404.16986(2024)

  6. [16]

    Nejati, A., Soudjani, S., and Zamani, M.Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems.European Journal of Control 57(2021), 82–94

  7. [17]

    M., et al.Julia: come for the syntax, stay for the speed.Nature 572, 7767 (2019), 141–142

    Perkel, J. M., et al.Julia: come for the syntax, stay for the speed.Nature 572, 7767 (2019), 141–142

  8. [18]

    Prajna, S.Barrier certificates for nonlinear model validation.Automatica 42, 1 (2006), 117–126

  9. [19]

    J.A framework for worst-case and stochastic safety verification using barrier certificates.IEEE Transactions on Automatic Control 52, 8 (2007)

    Prajna, S., Jadbabaie, A., and Pappas, G. J.A framework for worst-case and stochastic safety verification using barrier certificates.IEEE Transactions on Automatic Control 52, 8 (2007)

  10. [20]

    A.Introducing SOSTOOLS: A General Purpose Sum of Squares Programming Solver

    Prajna, S., Papachristodoulou, A., and Parrilo, P. A.Introducing SOSTOOLS: A General Purpose Sum of Squares Programming Solver. InConference on Decision and Control(2002), vol. 1, IEEE

  11. [21]

    A., and Dos Santos, P

    Ramos, J. A., and Dos Santos, P. L.Mathematical modeling, system identification, and controller design of a two tank system. In2007 46th IEEE Conference on Decision and Control(2007), IEEE

  12. [22]

    Rew, R., and Davis, G.Netcdf: an interface for scientific data access.IEEE computer graphics and applications 10, 4 (1990)

  13. [23]

    [24]Schneeberger, M., Dörfler, F., and Mastellone, S.Sos construction of com- patible control lyapunov and barrier functions.IFAC-PapersOnLine 56, 2 (2023), 10428–10434

    Santoyo, C., Dutreix, M., and Coogan, S.A barrier function approach to finite-time stochastic system verification and control.Automatica 125(2021). [24]Schneeberger, M., Dörfler, F., and Mastellone, S.Sos construction of com- patible control lyapunov and barrier functions.IFAC...

  14. [25]

    J., and Lall, S.Satisfiability

    Soroka, E., Kochenderfer, M. J., and Lall, S.Satisfiability. jl: Satisfiability modulo theories in julia.preprint arXiv:2309.08778(2023)

  15. [26]

    In2018 Annual American Control Conference (ACC)(2018), IEEE, pp

    W ang, L., Han, D., and Egerstedt, M.Permissive barrier certificates for safe stabilization using sum-of-squares. In2018 Annual American Control Conference (ACC)(2018), IEEE, pp. 585–590

  16. [27]

    S., Hu, H., Niu, P., Luo, X., and Liu, C.Modelveri- fication

    Wei, T., Marzari, L., Yun, K. S., Hu, H., Niu, P., Luo, X., and Liu, C.Modelveri- fication. jl: a comprehensive toolbox for formally verifying deep neural networks. arXiv preprint arXiv:2407.01639(2024)

  17. [28]

    Wooding, B., Horbanov, V., and Lavaei, A.Protect: Parallelized construction of safety barrier certificates for nonlinear polynomial systems.arXiv preprint arXiv:2404.14804(2024)

  18. [29]

    linear

    Zhang, H., Weng, T.-W., Chen, P.-Y., Hsieh, C.-J., and Daniel, L.Efficient neural network robustness certification with general activation functions.Advances in neural information processing systems 31(2018). A Benchmarking Setup StochasticBarrier.jl is also equipped with an i...

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.