Proof complexity in formal verification

Why some proofs don’t converge — and what to do about it

When a proof doesn’t converge, the first instinct is often to blame the tool. In reality, the structure of the problem is usually the main driver of complexity.

A simple 2D model

Proof complexity in formal verification can be understood using two dimensions:

Sequential depth: how many cycles the property needs to explore
Arithmetic complexity: how complex the datapath is

Where formal works best

Low depth and simple logic (e.g., FSMs, control logic, protocol checks) are typically easy for formal tools and converge quickly.

Where problems start

As designs require deeper sequential reasoning or include more complex arithmetic, proofs become harder and less predictable.

The danger zone

The most difficult problems combine deep pipelines with complex arithmetic, such as floating-point units with long latencies. These are inherently hard problems.

Practical strategies

If sequential depth is the issue:

Break properties into smaller steps
Add helper assertions (invariants)
Reduce the number of cycles the tool must explore

If arithmetic complexity is the issue:

Abstract datapaths
Black-box complex logic
Focus on control behavior instead of exact values

If both dimensions are high:

Decompose the design
Verify blocks independently
Use abstraction and refinement

Key takeaway

Don’t start by tuning the tool. Start by understanding where your problem sits in this space. Once the structure is clear, convergence becomes much more predictable.

One sentence to remember

With the right decomposition and abstraction, formal can turn even complex verification problems into focused, manageable proofs.