Skip to content
SPECIFICTION
Get listed

SeaHorn

seahorn.github.io

macOSLinuxSelf-hosted
Visit seahorn.github.io
Spec score 7.2 #17 of 25 in C and C++ Static Analysis Tools

What it is

SeaHorn is a free, open-source framework for automated analysis of C and other LLVM-based programs, developed mainly for research in automated verification. It is not an out-of-the-box static analyzer. Its frontend prepares LLVM IR bitcode, and its middle end converts optimized bitcode into verification conditions written as Constrained Horn Clauses. Backend engines use SMT-based model checking, including PDR/IC3 techniques, and CRAB can provide numerical invariants through abstract interpretation. SeaHorn supports abstract interpretation, context-sensitive pointer analysis, bounded model checking, constrained-Horn-clause software model checking, and termination or non-termination analysis. For C programs with assertions, `sea pf` translates the program, generates and solves verification conditions, displays invariants for safe results, or saves a counterexample for violations. `sea inspect` reports program structure and can produce memory or call-graph data. The framework also checks generated clauses for inconsistent code fragments using path coverage. Docker is described as the easiest starting point, with a nightly image refreshed daily. Building requires LLVM, Z3, and Boost, whose exact versions change. SeaHorn runs on Linux, macOS, or self-hosted systems under a modified BSD license.

Spec sheet

Purpose
SeaHorn is a verification framework for LLVM-based programs.Read 10 Oct 2026 · seahorn.github.io
Platforms
The README includes build instructions for Linux and a separate section on compiling on a Mac.Read 9 Oct 2026 · github.com
Integrations
The site identifies CRAB as the abstract interpretation analyzer SeaHorn uses to provide numerical invariants.Read 10 Oct 2026 · seahorn.github.io
Support
The project says it provides support to new users and invites users to report issues when Docker tags become stale.Read 9 Oct 2026 · github.com
License
SeaHorn is distributed under a modified BSD license.Read 9 Oct 2026 · github.com
Additional analysis
SeaHorn’s `sea inspect` command can report program structure and generate memory or call graph data.Read 9 Oct 2026 · github.com
Analysis engines
Its backend uses SMT-based model checking engines based on PDR/IC3, and uses CRAB to provide numerical invariants through abstract interpretation.Read 10 Oct 2026 · seahorn.github.io
Analysis output
The `sea pf` command can display computed invariants for a safe result or save a counterexample for a violation.Read 9 Oct 2026 · github.com
C verification
Its `sea pf` command takes a C program with assertions, translates it to LLVM bitcode, generates verification conditions, and solves them.Read 9 Oct 2026 · github.com
Counterexamples
SeaHorn can produce executable counterexamples when it finds a violation.Read 9 Oct 2026 · github.com
Dependencies
Building SeaHorn requires LLVM, Z3, and Boost; its README says the exact library versions change.Read 9 Oct 2026 · github.com
Download
The site links to a SeaHorn Docker image described as SeaHorn for LLVM 3.8; Docker Hub shows the nightly image command as `docker pull seahorn/seahorn:nightly`.Read 10 Oct 2026 · hub.docker.com
Founders
The site lists Arie Gurfinkel, Temesghen Kahsai, and Jorge Navas as founders.Read 10 Oct 2026 · seahorn.github.io
Frontend
Its frontend takes an LLVM-based program such as C and generates LLVM IR bitcode, preprocessing and optimizing it for verification.Read 10 Oct 2026 · seahorn.github.io
Image status
Docker Hub says the SeaHorn image was updated about 7 years ago and lists its size as 642.7 MB.Read 10 Oct 2026 · hub.docker.com
Inconsistency checking
SeaHorn detects inconsistent code fragments by computing path coverage for generated Horn clauses.Read 10 Oct 2026 · seahorn.github.io
Model checking
SeaHorn supports SMT-based bounded model checking and constrained Horn clause based software model checking.Read 9 Oct 2026 · github.com
Not a turnkey analyzer
The project says SeaHorn is not an out-of-the-box static analysis tool.Read 9 Oct 2026 · github.com
Optional analysis component
Crab abstract interpretation is optional and can supply invariants to SeaHorn’s Spacer backend.Read 9 Oct 2026 · github.com
Pricing
The opened official site provides a Download section but no pricing information.Read 10 Oct 2026 · seahorn.github.io
Static analysis
Supported features include abstract interpretation based static analysis and context-sensitive pointer analysis.Read 9 Oct 2026 · github.com
Termination analysis
SeaHorn can prove termination and non-termination by synthesizing and validating candidate ranking functions or producing a witness for non-termination.Read 10 Oct 2026 · seahorn.github.io
Use case
The site describes SeaHorn as a framework for analyzing programs and cites detecting abnormalities and serious bugs as a use of inconsistency checking.Read 10 Oct 2026 · seahorn.github.io
Verification conditions
Its middle end converts optimized LLVM bitcode into verification conditions expressed as Constrained Horn Clauses.Read 10 Oct 2026 · seahorn.github.io

Strong points and limits

Strong points

  • Supports multiple verification methods
  • Produces executable counterexamples
  • Can display computed invariants
  • Checks termination and non-termination
  • Docker distribution available

Limits

  • Not a turnkey static analyzer
  • Build dependencies and versions change
  • Docker image updated about seven years ago

Who it suits

It suits researchers and engineers assembling verification workflows for C or LLVM-based programs. Users should expect framework-level configuration rather than a turnkey analyzer.

Verdict

SeaHorn offers a broad, research-oriented verification framework with model checking, invariants, and counterexamples. Its non-turnkey design and changing build dependencies make setup part of the work.

Where Specifiction places it

Alternatives to SeaHornAll alternatives →