Formally verified models have a serious place in modern software dev, though they're often relegated to academia. One great use case is modelling critical components of your system in a proof assistant language, proving its correctness, and then using that model as an oracle in a differential fuzzing setup, detecting drift in the real implementation from the ideal, verifiably correct behaviour.

The linked repo has a minimal reference architecture for a ledger system, modelled and proven in Lean 4, and also implemented in Rust with intentional bugs. The repo also contains a small differential fuzzing suite, which you can run to visualise how we can detect bugs in the implementation by comparing behaviour to the model.

Let me know if you have any questions or suggestions :)