The complexity and low level of detail of software often require that together with reasoning logics we use additional techniques to simplify the verification. One of the most well known techniques is refinement between layers of specifications where the desired properties are verified on abstract specifications down to concrete implementations. This technique has been successfully applied on several system such as the SEL4 micro-kernel verification, Compcert, and CertiKOS, among others. 

Despite of the good results obtained by refinement between layers of specification, abstraction layers must be constructed manually, and it is necessary to construct and apply additional verification artefacts to show that properties are applied among layers. Moreover, the gap between the implementation and the highest level of abstraction is often too large to apply one level of refinement and it is necessary to apply different abstractions. As a consequence the verification effort is too big and it becomes necessary to obtain more efficient techniques.

In this talk I introduce phi-types together with phi-SL, a novel separation-based logic that allows to verify directly low level implementations while reasoning on abstract levels without having to construct additional specification layers. Phi-types embed the abstraction on hoare-triplets and introduces a consequence rule that allows to shift between different abstractions. We implement phi-types and phi-SL in Isabelle/HOL together with a layer of automation that allows the verification of complex systems with relatively low effort. Using phi-systems we have verified a large portion of the Uniswap protocol for smart-contracts. Uniswap encodes in Solidity a very complex financial model resulting in a very challenging verification, which we successfully carry out in our framework with very good automation.