Ah, sorry. Happy to explain any pieces in more detail. I hope the core is clear: If you think of Dapps as servers, then it synthesizes its clients (specifically ones that cause assertion failures).

For bugs: The demo videos on the FAQ page show the kinds of bugs it can find, e.g., the one that crashed the DAO, and ones that simpler tools will be unable to find. Of course you are right, the holy grail is finding bugs that escape both human audits and other tools. Haven't run it on very large codebases yet. Working on it!