Embed Notice

Is there any open source tool for proving assertions about machine code programs, given some minimal constraints (e.g., no self-modifyimg code, all computed branch targets identified)? Assertions like "the carry flag will always be clear when this instruction starts execution".

Open source needed because I'd want to adapt the tool for a proprietary and very unconventional processor architecture.