I'll provide more info once I'm finished doing some verification of Nim C
output.
"constant time stuff" \- no, I don't know such a tool. Static verifiers are
only looking for code correctness, e.g. proper mem. boundaries, reachability,
loop invariants, etc. If you want to verify things like constant time operation
I'd suggest a modelling tool to check your model ("algorithm"). Note that some
MVs can also produce code.
"non-verified compiler" \- a) there are some (very few) verified compilers,
e.g. CompCert.
b) _THE_ source of errors are still us humans, so verifying source code
produced by humans (or not properly tested generators) will lead to catching
and avoiding 99.x% of bugs/vulnerabilities.
The real problem is IMO that static as well as dynamic analyzers are relatively
complicated (to use and understand) beasts and to use them properly one must
understand quite a bit of formal methods and hence math (e.g. FOL, H3,
separation logic) - hence most developers do not use those tools.
One hint I can provide (in terms of _easy to use_ verifiers) is facebooks
"infer" tool. Be aware though that infer is rather limited, but it's very easy
to use and it seems to catch at least the more common (albeit simple) errors.
