With the recent rangeproof inflation bug, there has been increased talk about ensuring the integrity of the chain in the face of possible undetected implementation errors.
I’m very interested in developing a principled approach to this problem.
We have a distinct advantage over many other formal proof / verification applications — we can have multiple implementations that are optimized for different aspects of the problem, and the ecosystem as a whole benefits from the superset of all of them. In particular:

Our existing implementations are computationally performant, but not proven correct.

We could create an additional “verifier” implementation where performance is (relatively) unimportant, but that has some level of correctness proof.
The idea is that the “verifier” implementation would be significantly slower, but could be optionally run by anyone who wishes to devote extra resources to helping ensure chain integrity. It would not necessarily be a meaningful part of consensus, but would act as a “canary” early warning that something may be wrong with the chain before serious damage could be done.
We could even start small by “rusting out” parts of the implementation: Small parts of the existing code could be replaced by small parts of verified / autogenerated code that that is less performant but more likely to be correct.
Questions:

What language(s) would be easiest to formalize our proofs in? I’m familiar with Coq and Lean, there may be others? Are there any particular language or library requirements for the type of proofs we would use? Good support for elliptic curves? (Though… we’re not necessarily trying to formally prove elliptic curve cryptography, just our additions on top of it. We can make some fairly broad axiomatic assumptions, and then just prove on top of those.)

Do we have any connections to mathematicians / mathyprogrammertypes who could help us with the formalization? (Kevin Buzzard of Lean’s amazing mathlib “math standard library” might have some pointers here.)

What options are available for code generation from these languages? Note that we can combine multiple target languages and be as esoteric as we like, as the resulting code will ideally be largely autogenerated. (Example: Coq to Haskell)

What are the most promising initial components of our constructions that can be piecemeal replaced?

What are the “scariest” / least proven parts of the implementations?

Are there any other approaches that could increase confidence in chain integrity that take advantage of additional processor cycles or probabilistic effects?

What is the prior art of formal methods as applied to cryptography and blockchains in particular?
Thanks to @oryhp for inspiration and talking through some of this with me!