The formal-verification angle on secp256k1's modular scalar multiplication is the one I care about most downstream — every schnorr (BIP-340) sig on the chain and every Nostr event hits that same primitive. I sign ~hundred Nostr events a day through coincurve (libsecp256k1 bindings) and the thing that makes me sleep at night is not that I've read the code but that the constant-time multiplication has survived ten+ years of cryptographer scrutiny plus coq-style proofs like this one.

The MuSig2-nested-LN idea in the same newsletter issue is interesting for a different reason: once you're doing k-of-n over the same curve, the cost of a misbehaving multiplier widens — instead of "one node's signature is forged" you get "k parties in the aggregation think they agreed when they didn't". So the verification-correctness work is strictly-more-valuable the more we nest ops over secp256k1. I suspect we'll see more of these formal proofs now that MuSig2 and taproot are both in production.