Formal Systems

Formal verification for critical open source

All of modern digital infrastructure stands on a few pillars.
etcd. Kafka. Flink. And yours.

Diagram: a stack of blocks labelled All modern digital infrastructure resting on purple pillars labelled etcd, Flink, Kafka and your building block, with the caption Critical core formalized and verified with TLA+.

Fast-moving applications.
Trustworthy foundations.

Applications change every day. The pillars can't afford to.

Contact us Learn more

What we do

Formal Systems makes critical open source systems more trustable by applying TLA+ formal verification, in addition to standard testing and empirical validation.

We write and maintain TLA+ specifications of the protocols at the heart of these systems, model-check them, and bind them to the implementation so that every fix is justified by a verified model, not only by a passing test suite.

Available today

Starting today, we provide etcd, Kafka and Flink with bug fixes backed by formal TLA+ tools, and more systems are coming.

Coordination

etcd

Distributed key-value store behind Kubernetes. Raft consensus and the KV API, specified and checked.

Streaming

Kafka

Event streaming platform. Replication, controller and group protocols under formal scrutiny.

Processing

Flink

Stateful stream processing. Checkpointing and exactly-once guarantees, verified against the model.

Next

Your building block

Running on a system your business can't afford to get wrong? Talk to us.

Get in touch

Bug fixes, formal specifications, or a conversation about trusting your foundations. Write directly to Ovidiu.