The iMdea Software Institute
The partnership with the iMdea Software Institute was announced some time ago. The iMdea research institute is one of the seven research centers that form the iMdea initiative. The iMdea initiative "is a project founded by the Madrid Regional Government, included in the IV Regional Plan of Scientific Research and Technological Innovation 2005-2008 (PRICIT), for the purpose of setting up advanced research centers and higher education and training in the Community of Madrid." (Source) The iMdea Software Institute recruits the best international talent to be at the forefront of research, to ensure that software is safe, reliable and efficient. iMdea has high expertise in distributed, decentralized and formally verified software.

iMdea has just revealed a sneak peak on what they're working on for the Tezos ecosystem. Tezos' native smart contract language, Michelson, facilitates formal verification, a methodology commonly used in mission-critical environments such as the aerospace, nuclear, and semiconductor industries. iMdea is now "working on different lines of applications of formal methods for Tezos smart contracts, including runtime verification for monitoring contract execution (for example for preventing pitfalls dynamically)"

"Monitors are a defensive mechanism. The main idea is to be able to take any smart contract and extend it with a protective wrapper that is executed at the end guaranteeing constraints of the execution (failing otherwise).
It is common that a contract calls another asking for information (and maybe paying beforehand for it), however, currently, there is nothing the contract can do if it does not receive a call back with the requested information. Monitors can ensure that the contract received the information it asked/payed for, and failing if it does not happen." - Source

Arthur Breitman mentioned the example of Flash Loans where monitors can be very usefully deployed.

Flash Loans
Flash loans is an absolute simple, yet genius use of smartcontracts. It enables you to loan AND pay back money in ONE transaction. Which sounds useless, but is far from that. Because this type of loans get payed back in the same transaction as the loan is given out, it means that collateral is not required. Collateral is normally necessary to ensure a loan is payed back. But since the smartcontract already ensures guarantees the loan is being payed back (in the same transaction), flashloans can function uncollateralized. Still sounds useless? Here it comes: ever noticed that certain exchanges have (small) differences in prices of BTC? (Or other cryptocurrencies) To profit from these price differences, you only need to make one transaction. Buy low, sell high. Instantly. And simultaneously, borrow money and pay back. Instantly. This type of loans only work on-chain. So this only works in blockchain applications, since blockchain is a specialized database that processes transactions in batches and registers the state of balances "instantly" or rather in blocks. Blocks are not formed instantly, but as far as the balance goes, the next formed block is like the next tick of the clock in the life of a blockchain ledger. There is the latest block and then the next, newly formed with nothing in between. This means that flash loans are a use-case that strictly work on-chain and will only work smart contracts. So this works for smartcontracts that trade price differences between DEXes for example.