Klever

1. The rest half of screen is intended for associated marks. But there is not any associated mark yet and you were not an expert for corresponding job to have a button to create them. Something (like my previous sentence) should be shown in such cases.
2. Normally users shouldn't click on notes (blue text) and warnings (red text). They should click on corresponding rectangles like for the rest of error trace lines. But this is impossible due to #7103. Clicking on notes and warnings should be use to get more details about implementation of model functions that is hidden by default. As for your question warnings (red text) show assertions violated. They are automatically propagated from the __VERIFIER_error() to nearest model function calls and they correspond to notes that precede __VERIFIER_error(). I don't see much sense in the requested improvement since those people who do need such the details should understand what are they while other users will no experience such the problems at all.
3. Ditto it is a detail that is normally hidden by default from the most of users.

BTW, implementation of ldv_assert() will be considerably changed when we will switch to so called multi-aspect verification. So it is better to postpone this issue anyway.