I think they're doing different things. What they have in common is that they both use SMT solvers for automation. Glancing at the abstract, it seems like Dam,

I think they're doing different things. What they have in common is that they both use SMT solvers for automation. Glancing at the abstract, it seems like Dam, Guanciale and Nemati proved correctness theorems about a tiny hypervisor in ARMv7 assembly, using SMT solvers to automate some of the proof. The C compiler is not involved. Whereas seL4 is written in C, and the correctness theorems are proved using the C code and the specification. There is a compiler that turns the C code into RISC-V machine code. Then the new tool chain proves the equivalence of the C program and the RISC-V binary emitted by the compiler, using SMT solvers to automate some of that proof.