CAmkES is good for building static embedded systems (excluding stuff
running in VMs), but can't really do anything more AFAIK. 

Yes, CAmkES is designed for static architectures, which is where we can give an assurance story.

If you want something dynamic, i.e. more resembling a full OS, then have a look at Genode. But then all assurance and ability to reason about security properties goes out of the window.

Gernot