This has been a long time coming. I started RadiiPolynomial.jl back in 2019 (first released in 2021) and kept putting off making an announcement because there’s always one more feature to finish first… Turns out that’s endless so here it is (even though this is not a 1.0-release and things will keep moving, the core components has matured enough to be worth sharing).
RadiiPolynomial.jl is a library for computer-assisted proofs in nonlinear analysis. Roughly speaking the idea is to “prove what is seen on the screen”, meaning that a true solution exists near a numerical approximation, with a rigorous explicit error bound. The strategy is a combination of spectral methods with a fixed-point argument (see here) and this package provides a set of tools for implementing this.
Left: a heteroclinic connection and the attractor of the Shimizu–Morioka system (reference).
Right: the family of choreographies connecting the figure eight to the Lagrange triangle, from the proof of Marchal’s conjecture (reference).
Both are proven with RadiiPolynomial.jl (figures were made with Makie.jl).
An important point to stress is that the numerical approximations can come from wherever you like, for example DifferentialEquations.jl, BifurcationKit.jl or DynamicalSystems.jl.
The documentation has a couple of examples.
The next step is to build ready-to-use tools for well-understood classes of problems (such as steady states, periodic orbits and invariant manifolds). The above Shimizu–Morioka paper is a first step in this direction.
Comments, questions and bug reports are all welcome 
!