Apkallu Labs
Request access

Verifier Workbench

Proves whether C code is safe, and shows exactly where it isn't. Each function is checked by a bounded model checker over a real SAT or SMT solver, every refuted obligation comes with the inputs that break it, and a model's fix counts only when the checker proves it removes the defect and changes nothing else.

Ask for a demo Source on GitHub
Engines
CBMC 5.95.1 · ESBMC 8.5
Solvers
MiniSAT · Z3 · cvc5 · Bitwuzla · Boolector
Models
Claude · ChatGPT · Gemini · self-hosted
Exports
SMT-LIB · PDF reports
Walkthrough

From C source to a proof you can hand over.

A live run on arith.c, the Workbench's sample file: two real defects and one clean function, checked by CBMC 5.95.1 over Z3 4.8.12.

01 · Verify

Counterexamples, not warnings

Paste C source or drop a .c or .h file, then pick the engine, solver and loop bound. Each function is verified on its own with arbitrary argument values, so library code without a main works, and only obligations located in that function count, which rules out vacuous proofs.

Here two obligations are refuted in 0.12 s. The sum in avg() overflows at a = b = −2147475457, and store() writes buf[16], one past the end of the array. Each finding shows the inputs that trigger it, in decimal and hex, and the path that reaches the failure.

2 refuteda=-2147475457idx=16

Checksbounds · pointer · div-by-zero · signed-overflow · unsigned-overflow · conversion · undefined-shift

Verifier Workbench in dark theme after a live run on arith.c: CBMC 5.95.1 with Z3 4.8.12 reports 2 refuted and 0 proved. The source marks the overflow on line 5 and the out-of-bounds write on line 13, the findings panel lists F-01 and F-02, and the Trace tab shows the counterexample a = -2147475457, b = -2147475457.
02 · Repair

Only a proved patch counts

Repair asks a model for a patch, then checks it mechanically. A rejected patch goes back to the model with the reason, for up to three attempts by default. The result is repaired only when nothing is refuted; unrepaired is a first-class outcome.

In this run the first patch fixes avg() but empties store(), and the behavior proof rejects it: store(idx = 13, v = 128) is well-defined in the original, but the patch leaves buf[13] different. The second widens the sum to 64 bits and tightens the guard to idx < 16. CBMC re-verifies it, with 0 refuted and 3 proved, and proves avg() and store() behave as before.

The model answers in this run are scripted, the way the Workbench's own tests exercise the loop: first a patch that must be rejected, then the fix.

0 refuted3 proved≡ behavior proved
Verifier Workbench in dark theme showing the patched arith.c as a diff: avg() now computes the sum in 64 bits and store() checks idx < 16. The agent log shows iteration 1 rejected because behavior changed, iteration 2 re-verified with all 3 obligations proved, the verdict Verified — patch held (re-checked by CBMC), and avg and store proved to behave as before.
03 · Report

Evidence you can hand to an auditor

Each run gets a printable report: the target, the checks and loop bound that applied, every proof obligation with its status and time, the counterexamples, the patch that held and the log of every attempt. Print it or save it as PDF.

Any single obligation can also be exported as SMT-LIB and re-checked with a solver of your choice.

3 VCs checkedunwind 16×PDFSMT-LIB
Verifier Workbench verification report for arith.c in light theme: 0 refuted and 3 proved, the checks and loop bound that applied, a table of proof obligations for avg and store, the patch that held as a diff, and the log of each repair attempt.
Guarantees

What “proved” means here.

A bounded model checker proves a property within bounds. Every result says exactly which bounds applied.

✓ harness#per-functionEach function on its own
Every function is verified with arbitrary argument values, so library code without a main works. Only obligations located in that function count, which rules out vacuous proofs of code the entry never reaches. Failures inside library code it calls, such as memcpy, are reported against it.
✓ outcomes#threeProved, refuted or inconclusive
Loops are unwound up to a bound, 16 by default, with unwinding assertions on. If a loop can run longer, that function's results are inconclusive, never proved; raise the bound to settle them.
✓ inputs#arbitraryArbitrary pointers
Pointer arguments are arbitrary, possibly NULL or dangling. Findings that depend on this carry a note, since the caller may guarantee a valid pointer.
✓ smtlib#exportRe-checkable by anyone
Every obligation exports as SMT-LIB. The formula asserts the obligation's negation: sat means it can be violated, and the model is a counterexample; unsat means it holds within the bound.
Verified repair

Every patch has to pass four checks.

A patch that passes all four, with strictly fewer refuted obligations, becomes the version the next attempt builds on. A rejected patch goes back to the model with the reason.

1 · guardsNo tricks
The patch may not add verifier intrinsics or assumptions (__CPROVER_*, __ESBMC_*, __VERIFIER_*, __builtin_assume), checker pragmas or inline assembly, calls that end the program such as abort() and exit(), includes outside the source, or macros that redefine existing names or keywords. Every assertion must stay as written and in force, so even #define NDEBUG is rejected.
2 · re-verifyRe-verified
The same engine, solver, bound and checks verify the patch again. Every function of the original keeps its exact type, and no obligation the original decided may become inconclusive.
3 · behaviorSame behavior, proved
CBMC proves that each changed function, and every function that calls one, returns the same value as the original, leaves the same global state and doesn't end the program where the original returns, on every input where the original has no undefined behavior and passes its assertions. A difference comes back as concrete inputs, and a proof that doesn't finish rejects the patch. Nothing submitted is ever executed.
4 · obligationsNo vanishing checks
If every obligation of a function disappears, the function must be proved equivalent to the original.
Limits

What it doesn't prove, yet.

Known limits, stated plainly rather than left to the fine print.

  • BoundsResults hold up to the loop bound. A loop that could run longer comes back inconclusive, not proved.
  • Skipped functionsThe behavior proof doesn't compare functions with pointer or struct parameters or results, variadic functions, or functions that reach one without a body. Results mark them skipped, and check 4 still applies.
  • Static localsFunction-local static variables aren't compared by the behavior proof.
  • Initial stateVerification and the behavior proof start every call from the globals' initial values.
  • Safety, not specsIt proves safety obligations such as bounds, overflow, pointer validity and division by zero, not that a function meets its specification. Function contracts are on the roadmap.
  • MISRAMISRA C:2012 rules aren't checked yet, and the Workbench says so instead of showing canned results.
Security

Built to analyze untrusted C.

✓ checkers#isolated

Isolated checkers

Checkers run in a private temporary directory with a memory cap and a timeout, and see none of the server's environment, API keys included. Includes of absolute or parent paths are rejected.

✓ code#never-run

Nothing executed

Submitted C is never run. The model only proposes code: checkers read it, and the behavior proof analyzes it symbolically.

✓ keys#server-side

Keys stay on the server

Model keys are configured on the server, and the API reports whether a provider is set up, never the key.

✓ runs#local

Your source stays with you

Runs, source included, stay in the browser that made them. The server stores none.

Status

Where it stands.

WORKING TODAY
  • Verification with CBMC and ESBMC: per-function harnesses, bounded outcomes and real counterexamples
  • Five solver back ends, and SMT-LIB export for every obligation
  • The guarded repair loop with behavior proofs, on Claude, ChatGPT, Gemini or a self-hosted model
  • The web app: new runs, the workbench, printable reports, and a recorded demo when no server is reachable
  • A Docker image with both engines and their solvers
Try it

See it on your own code.

Tell us about the C you'd like checked, and we'll walk you through a run: the findings, their counterexamples, and a repair only if the checker proves it.

Ask for a demo Source on GitHub