EDIT nov-02-2021: I misspoke earlier, details at the bottom.
Cardano is not intrinsically flashloan-attackless. Functional programming and formal verification help you a lot with the distance between spec and implementation, but do not give you anything with the distance between reality and spec. Reality (edge cases, attackers, things you failed to foresee) will be what gets you if your devs didn't let a simple bug through. Any proof engineer will tell you that false sense of security is a risk introduced by formal verification
It's tricky because we only use one word: "exploit" - when what we mean is either exploits at the software implementation level or exploits at the mechanism design level, but not both. The literature is infused with ambiguity, one must read diligently if they want to disambiguate this.
If you make progress on this, charge someone a lot of money.
EDIT: Cardano is in fact intrinsically flashloan-attackless at this time, but it is not because of "formal verification", it's because there are no multi-step yet atomic transactions. Flashloans, by definition, are an atomic transaction where an uncollateralized loan happens in the first step and it gets repaid in the last step. No multi-step yet atomic transactions, no flashloans, no flashloan attacks.