A static analysis reasons about code without running it. Static analyses can be used to find bugs, enforce style guides, or even prove that code can't have certain kinds of bugs.
One common kind of static analysis is a linter - a syntactic analysis. A linter only looks at what the code looks like - it doesn't try to understand the code at all. Linters are commonly used to enforce style guides.
Some example linters that are widely used in industry:
Another common kind of static analysis is a heuristic bug finder. These tools are semantic - unlike linters, they actually try to understand the code they are examining. Their goal is to find as many bugs as possible without introducing too many false positives.
Some examples of industrial-strength bug finders:
More heavy-weight static analyses can be used to prove facts about code. They require more input from the programmer (usually correlated to the difficulty of the property being proved), but are "sound" - they never miss bugs, unlike bug finders.
Some examples of static analyses that can produce proofs that scale to industrial codebases:
Verification is another way to prevent bugs in your software. However, verification needs writing precise specification (typically in a formal logic language), or add annotations (e.g. assert) inside code. Sometimes you can verify certain properties of your software automatically, sometimes you need to manually verify it, normally using some proof assistants.
Some examples of verification tools and projects:
Project ideas: