The last paper in my post here might be useful, take that paper and pop it into scholar.google.com and see if there’s anything there.
However, you could also combine that with the “using high level language as a cross assembler” (SPARK annotating the ‘assembly’ subprograms), and proving that.