In argotorg/solidity#1178 there is a plan to export annotated opcodes from the Solidity compiler.

This issue keeps track of performing an experiment of verifying a program snippet with interleaved static assertions. See the proposed syntax in argotorg/solidity#1178.