Formal Verification for Production APIs
Your tests check
what you wrote.
Proof checks
what you meant.
Proof translates your API contracts into formal specifications and uses model-checking to verify your implementation is correct by construction — not by coverage.
No deployment required
Fixed scope, fixed fee
4-week delivery
{
"subsystem": "auth-middleware",
"findings": [
{
"id": "G-001",
"category": "specification_gap",
"severity": "high",
"description": "Nil-pointer dereference on
empty Authorization header",
"realizable": true,
"kind2_output": "INVALID"
},
{
"id": "G-002",
"category": "missing_invariant",
"severity": "medium",
"description": "Token expiry not enforced
in refresh flow",
"realizable": true
}
],
"coverage": "7 / 7 categories",
"elapsed_minutes": 118
}02 / METHODOLOGY
From contract to proof
in five steps.
Proof doesn't generate test cases or scan for known CVEs. It formally verifies that your implementation satisfies your specifications — producing machine-checkable evidence, not a confidence score.
Specify
We translate your OpenAPI / AsyncAPI contracts and business rules into formal LTL/CTL specifications using Kind2 and TLA+.
Realizable?
Before checking correctness, we verify the specification itself is satisfiable — so you know the spec is actually achievable.
Verify
Model-checking exhaustively explores all reachable states of your implementation against every property in the spec.
Trace
Every finding links back to the specific requirement it violates, the code path that triggers it, and a reproduction scenario.
Evidence
You receive a gap analysis report, Kind2 counterexample output, trace links, and an executive summary — all auditable artifacts.
03 / WHY PROOF
The five properties that
separate Proof from a pentest.
Deterministic
Same inputs, same verdict. Proof's analysis is purely algorithmic — no probabilistic sampling, no false-positive rate.
Evidence-first
Every finding is a machine-checkable artifact: a counterexample trace, a gap reference, and a reproduction path.
Complete
Model-checking exhaustively explores all reachable states. There is no coverage percentage — either the property holds or a counterexample exists.
Traceable
Each finding maps to a named requirement, a line of code, and an execution trace — giving your team an unambiguous fix target.
Accountable
The report is a signed artifact you can share with customers, auditors, or acquirers. It carries our name on the methodology.
04 / CASE STUDY — TYK API GATEWAY
A production bug found
in 2 hours. Zero Tyk
engineers involved.
Proof was run against the Tyk API Gateway — a production open-source codebase — without any involvement from the Tyk team. No deployment. No access. Just the source.
A nil-pointer dereference bug and a specification coverage gap were identified in approximately 2 hours. Tyk's own test suite had not caught it. No prior security review had surfaced it.
Time to first finding
2h
Nil-pointer dereference, Auth middleware
Tyk team involvement required
None
Source access only. No deployment, no calls.
Test suite coverage of the bug
0%
Not caught by 1,200+ existing unit tests.
05 / THE SERVICE
Proof Audit —
fixed scope, fixed fee.
Every engagement is fixed-scope and fixed-fee. You know exactly what you'll receive before we start. No open-ended retainers, no hourly billing, no hidden scope creep.
Pilot
$5,000
Single endpoint or small state machine. Proof of concept for your team.
- ✓1 endpoint or state machine
- ✓Gap analysis report
- ✓Kind2 counterexample output
- ✓Executive summary
- ✓4-week delivery
Single Subsystem
$15–25k
One bounded subsystem — auth, billing, rate-limiting, or similar.
- ✓1 bounded subsystem
- ✓Full specification coverage report
- ✓Trace links for all findings
- ✓Reproducible counterexamples
- ✓4-week delivery
Extended Audit
$35–60k
Multiple interconnected subsystems with cross-boundary invariants.
- ✓2–4 subsystems
- ✓Cross-boundary invariant checking
- ✓Priority fix ordering
- ✓Sign-off artifact for customers/auditors
- ✓6-week delivery
Retainer
$8–15k/mo
Ongoing coverage as your API evolves. New endpoints verified continuously.
- ✓Continuous spec tracking
- ✓Monthly gap analysis diff
- ✓Priority findings within 48h
- ✓Architecture review included
- ✓Rolling monthly
All tiers: contact audit@reqproof.com to start.
GET STARTED
Pentests find known patterns. Proof finds gaps you did not know existed.
Send us your OpenAPI spec or codebase and we will respond with a scoping assessment within 48 hours. No obligation.