ACKNOWLEDGEMENTS

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108), from AUFF, and from Arm, Google, and Amazon.
The authors would like to thank the Isaac Newton Institute for Mathematical Sciences, Cambridge, for support and hospitality during the programme Big Specification: Specification, Proof, and Testing at Scale, where some of the work was undertaken.
This work was supported by EPSRC grant EP/Z000580/1 and Samsung Research Funding Center of Samsung Electronics under Project Nubmer SRFC-IT2102-03.