Trying to write a formally verified simplified (1D) implementation of Ruckig, more to learn the tools than for the result, although I want that too. Some fun challenges with numeric stability (using the big hammer of arbitrary precision to address that for now), etc. Still don’t have a real path to bridge correctness arguments through a formalization of Sturm’s theorem or similar, accepting it as an axiom for now.