Schematic Book a demo

Schematic Research

Intelligence,
with proof.

AI that verifies software and proves mathematics.

See it in action Book a demo
ObserveGeneraliseVerify
SOFTWARE MATHEMATICS VERIFIED

What we build

From claim
to certainty.

Follow a claim from input to verification.

Sentry and Hydra put our proof engine to work.
Explore Sentry Explore Hydra
01 / 03

Observe

Read the code and the tests that already exist.

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 behaviour

Products

Built for hard
questions.

Hydra finds formal proofs. Sentry brings that certainty to software.

01
SOFTWARE ASSURANCE

Sentry

Find what tests miss.

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

Hydra

Proof as an API.

Hydra is the autonomous proof engine inside Sentry – and available directly for mathematics.
Formalise→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 optimisation.

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 programme 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 Colour Theorem

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

Hydra
02Graph theory

Dominating Four Colour

New mathematical work developed alongside its machine-checkable proof.

Research
03Systems software

Pinned C semantics

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

Sentry
04Software laws

Universal test corpora

Thousands of examples consolidated into compact, parameterised claims.

Supertests

The team

Built by people
who prove things.

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