World's first
End-to-end C project
formal verifier
Giolit Program Verifier 7.0
Proof your software can't fail — or see the exact input that breaks it.
Testing tries a few inputs. Giolit proves what happens for all of them — every input, every path, every thread timing across your whole C project. You get proof it can't fail, or the exact input that breaks it.
v7 7.0.0 (trial) · Linux x86-64 · exit codes for CI · SARIF for GitHub & GitLab · C++ SDK
Complete C projects formal verifier
Whole projects, not just single functions.
- Until now only single functions could be formally verified — Giolit Verifier verifies end-to-end projects spanning multiple files.
- The C project may include multiple threads or recursions, multiple functions and multiple files.
- Proof for every input, not a sample — or the real bug with the exact failing input, never a false alarm.
- Evidence, not opinions: a certificate your auditors can check.
$ v7 a.c b.c -I include -D CONFIG=1
$ v7 --entry=my_func src/*.c
$ Result — 177 benchmarks, 0 wrong answers
102 programs proven safe · 75 real bugs found with the failing input · overflow, division by zero, array-bounds, pointer safety, memory leaks — automatically on Ubuntu 24.04.
Proof for every input
Proves absence of run-time errors in C — overflow, division by zero, array-bounds, pointer safety, memory leaks — for every input, not a sample.
Fast answer, or the failing case
Several proof strategies run at once — the first answer wins. You get proof it can't fail, or the exact input that breaks it.
Auditable Certificates
Every run yields a PDF certificate or counterexample report with the proof on the control-flow graph, plus JSON, SARIF 2.1.0 and the full proof.
Built for Safety Standards
Evidence ready for ISO 26262, DO-178C, IEC 61508 & IEC 62304 reviews — with CI exit codes, SARIF gates and a C++ SDK.
C verification benchmarks
Proven on 177 C benchmarks — zero wrong answers.
Testing samples. Proof covers every input, not a sample — measured here on 177 programs. 75 are real bugs with the exact failing input, never a false alarm. Every benchmark ships in the trial with its known answer and full result bundle, so you can re-run the evidence yourself with v7 file.c. Median verification time is about 10 seconds per benchmark.
177
C benchmarks with known answers
102
programs proven safe (PROVEN)
75
real bugs found with failing input (VIOLATED)
~10s
median verification time per benchmark
Blazing fast
Answers in seconds, not hours.
Proof for every input, not a sample — or the real bug with the exact input that breaks it, never a false alarm — in seconds, with evidence your auditors can check. Several proof strategies run at once, and the first answer wins.
~10s
median per benchmark (177 benchmarks, zero wrong answers)
0.5s
concurrent proof: 2 checks PROVEN (mutex threads)
16s
35-file project proof: 9 checks PROVEN, 4870 lines linked
177 / 0
benchmarks / wrong answers — 102 safe, 75 bugs with failing input
For experts: a portfolio of invariant, contract, Owicki–Gries and CEGAR engines plus random interleavings and byte-exact execution races in parallel — first decision wins. Re-run every benchmark in the trial.
Complete C projects formal verifier
Complete C projects formal verifier — end to end, like your build.
Your whole project, checked the way you build it — proof for every input, not a sample, or the real bug with the exact failing input, never a false alarm, plus evidence your auditors can check. World's first end-to-end C project formal verifier: until now only single functions could be formally verified — Giolit Verifier verifies end-to-end projects spanning multiple files. The C project may include multiple threads or recursions, multiple functions and multiple files. v7 compiles and links all your files exactly as in a normal build — v7 a.c b.c -I include -D CONFIG=1 — verify a single function for every caller with --entry while still linking the whole project.
Multi-file compile + link
Every translation unit with its -I and -D flags, linked end to end — src/*.c with -Iinclude, just like your Makefile.
Multiple threads, proven
POSIX threads, mutexes, C11 atomics and lock-free protocols checked across every timing — races surface with the failing timing. Expert detail: Owicki–Gries proofs.
Recursion with auto contracts
Recursive functions verify against auto requires/ensures contracts instead of unrolling forever.
Multiple functions, every caller
Functions across files verified together; --entry=my_func proves one function for every caller while the full project stays linked.
kvserver scale QA
Proven at kvserver project scale.
kvserver scale QA: ~8,400 lines across 34 modules — 3 clients, 3 workers, monitor, replicator — with 7 planted bug variants and 1070 unit checks. The project certificate below links 35 files / 4870 lines end to end for entry kv_fletcher16_words in 16s: 9 proven / 0 violated, issued under license GIOLIT-PRO-2026-000011.
Small end-to-end projects
Multi-file examples in the trial.
- Bank transfer — conservation across files — balances preserved end to end
- Protocol FSM — state-machine safety across translation units
- Sensor limiter — threshold logic with multi-file sensor pipeline
- Ring buffer — bounded-buffer correctness with producer/consumer files
What it checks
Every way your code can fail — checked in one run.
If it can crash, leak, or go wrong — it's checked. One run checks all eight run-time error families at once — for every input, every path and every thread interleaving. Each check ends PROVEN, VIOLATED (with the exact failing input and step-by-step trace), UNREACHABLE or UNKNOWN within your --timeout budget. Select a subset anytime with v7 --checks=overflow,valid-deref file.c.
Assertions and functional properties ride on top: assert() and reach_error() are verified for every caller — including multithreaded POSIX-threads code with mutexes, C11 atomics and lock-free protocols. Download the trial and run the checks.
The product
Testing tries some cases. Proof covers every case.
Testing checks the inputs you thought of; the verifier checks all of them — all 2³² values of an int, every loop iteration, every schedule of your threads. Giolit Program Verifier brings sound formal reasoning into the software engineering workflow: PROVEN is never wrong (sound over-approximation), and VIOLATED is never a false alarm (every counterexample is replayed on exact C semantics before it is reported).
World's first end-to-end C project formal verifier, built for high-assurance environments — embedded controllers, automotive (ISO 26262), avionics (DO-178C), industrial control (IEC 61508) — the Verifier turns every run into evidence, not opinions: a certificate your auditors can re-check, or the real bug with the exact failing input, never a false alarm.
Detail for experts: PDF certificate or counterexample report with the proof drawn on the control-flow graph, plus JSON, SARIF 2.1.0 and the full proof.
Verification flow
From program to evidence.
Source
C program
Analyse
Program model
Verify
Formal reasoning
Check
Evidence
Report
Actionable result
What it brings
One run. Every input. Every path. Every thread timing.
Testing samples. Proof covers every input, not a sample — the verifier proves absence of run-time errors instead of sampling for them. You get the real bug with the exact failing input, never a false alarm, plus evidence your auditors can check.
For experts: a portfolio of proof engines (invariants, contracts, Owicki–Gries, CEGAR), random thread interleavings and byte-exact execution race in parallel — first decision wins.
Integer overflow & arithmetic safety
Signed overflow, division by zero and invalid shifts detected for every input value — the classic C run-time errors compilers leave undefined. Expert detail: CWE-190, CWE-369.
Memory safety: bounds, pointers, leaks
Array-bounds violations, null/dangling pointer dereferences, double/invalid free and memory leaks, each with the exact failing input and trace. Expert detail: CWE-787, CWE-476, CWE-401.
Concurrent C verification (POSIX threads, C11 atomics)
Multithreaded programs verified across every timing — mutexes, atomics and lock-free protocols included, with the failing timing when a race exists.
Proof certificates auditors can re-check
PDF certificate or counterexample report with the proof on the control-flow graph. Detail: plus JSON, SARIF 2.1.0 and proof.json.
CI gates & SDK integration
Proof that fits your pipeline: green means proven for every input, red means a real bug with the failing input. Detail: exit codes gate your build (0 proven, 1 violated, 2 unknown), SARIF uploads to GitHub & GitLab, and a C++ SDK (verify_file, unit_check, certify, ci_gate).
Safety-standard evidence (ISO 26262, DO-178C)
Formal proof recognised as evidence by DO-178C, ISO 26262 and IEC 61508 — produced as signed certificates ready for reviews and safety cases.
Designed for
Built for real C projects — big, multi-file, multi-thread.
If it's real C code — one file or dozens, one thread or many — it fits. Sequential C, recursive functions, multithreaded POSIX-threads code, multi-file projects linked as in your build, and single functions verified for every caller with --entry. Inputs are nondeterministic values, entry-function parameters, volatile variables and external data — constrained with __VERIFIER_assume. The trial package demonstrates each class with runnable examples.
Verification outcomes
The selected property is established under the verification model.
A concrete failing behaviour can be reported when a property does not hold.
The relevant operation cannot be reached from the analysed entry point.
The analysis remains undecided within the configured verification budget.
One command
One command. A clear answer: proven, or broken with proof.
No annotations, no harnesses. Point v7 at your C files and get a clear answer per check — proven for every input, or broken with the exact failing input and every step, plus a certificate your auditors can check.
Detail: PDF certificate + JSON, SARIF and proof in --report=DIR with CI-ready exit codes.
$ tar xzf giolit-verifier-7.0.0-trial.tar.gz && ./install.sh
$ v7 examples/safe.c
[overflow] PROVEN — no signed overflow on any input
[valid-deref] PROVEN — no null/dangling access on any path
VERDICT: PROVEN (exit 0) — certificate.pdf + results.json + report.sarif + proof.json
$ v7 examples/bug.c --report=out
[overflow] VIOLATED — x = 2147483647, x + 1 overflows (trace: main:7 → add:3)
VERDICT: VIOLATED (exit 1) — counterexample report with failing input + every step
$ v7 --license
trial: 982 runs left, 47 days left (uses no runs)
Example certifications
Real certificates: PROVEN or VIOLATED with full evidence.
Proof you can hand to an auditor — or the exact failure, step by step, never a false alarm. Every verification yields a certificate or report with evidence you can re-check. These are real pro-engine outputs, issued under license GIOLIT-PRO-2026-000011: concurrent proof, race violation with the failing timing, and a multi-file project proof linking all files end to end.
Detail: full evidence — PDF + results.json + SARIF 2.1.0 + proof.json + sources + reproduce.sh.
PROVEN
Concurrent mutex — all checks proven
2 PROVEN / 0 violated · 0.5s · 1 file · 25 lines
06_threads_mutex.c (entry main)
Download PDF
VIOLATED
Threads race — violation found
1 violated + failing interleaving (2 checks: 1 proven, 1 violated) · 0.3s · 1 file · 23 lines
07_threads_race.c (entry main)
Download PDF
PROVEN
kvserver project — per-function proof
9 proven / 0 violated · 16s · 35 files / 4870 lines
2186 checks: 9 proven, 0 violated, 2177 unreachable · entry kv_fletcher16_words · -DKV_SEQUENTIAL -Iinclude · license GIOLIT-PRO-2026-000011
Download PDFCI, SARIF & SDK
Proof that fits your pipeline.
Verification belongs in your pipeline, not on a side desk. Green means proven for every input, red means a real bug with the exact failing input, never a false alarm — plus a certificate your auditors can check.
Detail: exit codes gate the build — 0 all proven, 1 violated, 2 unknown, 3 usage error, 4 no license — while --sarif output uploads straight to GitHub code scanning or GitLab. A public C++ SDK (verify_file, unit_check, certify, ci_gate) lets you embed the C verifier in your own tools.
Pipeline snippet
$ v7 src/*.c --timeout=300 --report=proof
$ test $? -eq 0 || exit 1 # fail build on VIOLATED
# upload proof/report.sarif to GitHub code scanning
Trial terms
System requirements and trial terms: Ubuntu 24.04, 1000 runs, 50 days.
The trial (giolit-verifier-7.0.0-trial.tar.gz) allows 1000 runs within 50 days on one Linux x86-64 computer — Ubuntu 24.04 LTS or newer, LLVM/Clang 18, libc6-dev, libssl3 (LuaLaTeX + qpdf for PDFs). It includes the v7 command, 12 tutorial examples, 177 benchmarks with known answers and every result bundle. v7 --license shows runs and days left without using a run.
FAQ
C verifier FAQ: proof, coverage, trial.
Short answers to the questions every team asks before trusting a C program verifier — what PROVEN means, what it covers, and what the trial includes.
What does Giolit Program Verifier prove about my C code?
01For every input, every path and every thread interleaving: no failed assertion, no signed integer overflow, no division by zero, no invalid shift, no out-of-bounds array access, no null/dangling pointer dereference, no double/invalid free and no memory leak. Each check ends PROVEN, VIOLATED (with the exact failing input and every step), UNREACHABLE or UNKNOWN within your --timeout budget.
How is this different from testing?
02Testing checks the inputs you thought of — the verifier covers all of them (all 2³² values of an int, every loop iteration, every thread schedule). PROVEN is never wrong (sound over-approximation) and VIOLATED is never a false alarm (every counterexample is replayed on exact C semantics). You get a PDF certificate with the proof drawn on the control-flow graph, plus JSON, SARIF and proof.json for independent re-checking.
Which C programs and inputs does it handle?
03Sequential C, recursive functions, multithreaded POSIX-threads code (mutexes, C11 atomics, lock-free protocols), multi-file projects linked as in your build, and single functions verified for every caller with --entry. Inputs are __VERIFIER_nondet_*() values, entry-function parameters, volatile variables and external data — constrained with __VERIFIER_assume(cond).
How do I run it and gate CI?
04v7 file.c [file.c ...] with --checks, --entry, --timeout and --report=DIR for the PDF + JSON + SARIF + proof bundle. Exit codes gate your build: 0 all proven, 1 violated, 2 unknown, 3 usage error, 4 no license. Upload --sarif to GitHub code scanning or GitLab, or embed via the C++ SDK (verify_file, unit_check, certify, ci_gate).
What is in the trial and what do I need to run it?
05giolit-verifier-7.0.0-trial.tar.gz: the v7 command, 12 tutorial examples, 177 benchmarks with known answers and every result bundle, plus Tutorial, Product Overview, README and License Terms. Trial = 1000 runs within 50 days on one Linux x86-64 machine (Ubuntu 24.04+, libllvm18, libclang-cpp18, libc6-dev, libssl3; LuaLaTeX + qpdf for PDFs). v7 --license shows runs and days left without using a run.
Which safety standards is it built for?
06Embedded controllers, automotive (ISO 26262), avionics (DO-178C), industrial control (IEC 61508), medical devices, protocol parsers, security boundaries and libraries with many callers. DO-178C, ISO 26262 and IEC 61508 recognise formal proof as evidence — the verifier produces that evidence as a signed certificate ready for audits and safety cases.
How does end-to-end C project verification work?
07v7 compiles and links all your files exactly as in a normal build — v7 a.c b.c -I include -D CONFIG=1 — spanning multiple threads (POSIX threads, mutexes, C11 atomics with Owicki-Gries proofs), recursion via auto requires/ensures contracts, and multiple functions across multiple files. Verify one function for every caller with --entry while still linking the whole project. Every run yields full evidence: PDF + results.json + SARIF 2.1.0 + proof.json + sources + reproduce.sh.
What does the kvserver project certificate prove?
08It links all 35 project files (4870 lines) end to end for entry kv_fletcher16_words: 9 proven / 0 violated in 16s, issued under license GIOLIT-PRO-2026-000011 — a per-function proof for every caller with the full project linked.
Commercial licensing
Prove your C code — start free
Bring Giolit Program Verifier into your high-assurance software workflow. Start with the free 1000-run trial for Ubuntu 24.04 — or talk to us about production licensing for your team and CI.