Schematic Book a demo

Schematic Research

Intelligence,
with proof.

AI for software verification and mathematical reasoning.

See it in action Book a demo
ObserveGeneralizeVerify
SOFTWARE MATHEMATICS VERIFIED

See it in action

Beyond
the test suite.

Schematic turns observed software behavior into a claim over every valid input, then searches for a proof or a concrete counterexample.

01 / 03

Observe

Start with source code and the tests that already pass.

Sentry
exchange-marshaller main
src/decoder.rs RUST
98fn decode_frame(bytes: &[u8], depth: usize) {
99  let header = parse_header(bytes)?;
100  verify_checksum(bytes, header)?;
101  if depth > MAX_DEPTH {
102    return Err(Error::TooDeep);
103  }
104  decode_children(bytes, depth + 1)
105}
Repository indexed
Imported tests
✓ roundtrip_empty_packet
✓ roundtrip_nested_packet
✓ roundtrip_binary_payload
✓ roundtrip_unknown_fields
27 examples ↓ one behavior

Explore the products

Built for hard
questions.

Sentry applies our proof engine to software. Hydra makes that engine available directly.

01
SOFTWARE ASSURANCE

Sentry

Find what tests miss.

Sentry discovers defects and turns important behavior into release-gating guarantees.
Discover→Generalize→Verify
Explore Sentry
02
PROOF INFERENCE

Hydra

Proof as an API.

Hydra is the autonomous proof engine inside Sentry – and available directly for mathematics.
Formalize→Search→Check
Explore Hydra

Research & results

Proof,
in practice.

Formal methods applied to real software and serious mathematics.

CASE 001HEATSHRINK · C

A passing test suite is evidence.
It is not a guarantee.

100M+ assertions passed.
The source was still wrong.

Exact source execution exposed a null access hidden by optimization.

COUNTEREXAMPLE VERIFIED
heatshrink_encoder.cFORMAL TRACE
584if (hse->match_scan_index > 0) { 585  uint8_t *buf = hse->buffer; 586  buf[hse->match_scan_index] = byte;← null 587}
×.nullPointerAccessreachable at source level
135universal claims
9public libraries
13,840cases · one proof
What these numbers measure +

The program spans pinned versions of nine open-source C, Rust and Python libraries. The 135 claims are compact universal properties consolidated from existing test corpora; exact formal coverage varies by library and is reported per result.

01Formal mathematics

Four Color Theorem

A complete formalization, built to be checked rather than taken on trust.

Hydra
02Graph theory

Dominating Four Color

New mathematical work developed alongside its machine-checkable proof.

Research
03Systems software

Pinned C semantics

Exact source behavior reproduced in Lean for real, widely used libraries.

Sentry
04Software laws

Universal test corpora

Thousands of examples consolidated into compact, parameterized claims.

Supertests

The team

People behind
the proofs

Mathematics, software and company-building experience in one research team.

Explore the team
Thanos Papaïoannou 01
CEO / TITLE / DESCRIPTION

Thanos Papaïoannou

Short two-line biography sits here when final roles and wording are approved.

Mark Kisin 02
TITLE / DESCRIPTION

Mark Kisin

Short two-line biography sits here when final roles and wording are approved.

Keeley Hoek 03
TITLE / DESCRIPTION

Keeley Hoek

Short two-line biography sits here when final roles and wording are approved.

Zoe Schwerkolt 04
TITLE / DESCRIPTION

Zoe Schwerkolt

Short two-line biography sits here when final roles and wording are approved.

Provisional portraits and biographies. Mark Kisin photograph: Renate Schmid, CC BY-SA 2.0 DE.

Start a conversation

What would you prove
if you could?

Book a demo