Linard Arquint

@jboillot I've attached the [compiled documentation](https://github.com/user-attachments/files/22003956/main.pdf). I'm using the branch of this PR, ran `cp -r ../../* .` in `examples/documentation`, and use `latexmk -pdf -shell-escape main.tex`. Could the difference be...

My comment goes in a similar direction as @Aurel300's: Imho Gobra already produces JSON output specifying what stuff did not get verified. Orthogonally, adding a bunch of `trusted` annotations all...

Regarding modularity, if you actually verify multiple packages (like Gobra supports), you could actually point out the remaining assumptions (unverified packages incl. standard library, abstract functions, ...)