We've talked about formal verification of the smart contracts.

We want to ensure that our smart contract doesn't lose money. While it's impossible to get a 100% proof of the absence of bugs, it's possible to test the critical parts of the contract using formal methods. Using formal methods = proving theorems about the contract code.

We're currently experimenting with Lean 4 for the purposes of the contract code verification. Our current goal is to build a model of the contract in Lean, prove theorems about the contract functions, then write a script that executes random transactions on the contract & checks that the output of those transactions is equal to the output of the Lean model (in other words: that Solidity code is equivalent to Lean code).

Again, this won't give us 100% guarantee, but it would give us a much higher assurance than regular testing.