Formal verification for critical open source
All of modern digital infrastructure stands on a few pillars.
etcd. Apache Kafka. Apache Flink. And yours.
Fast-moving applications.
Trustworthy foundations.
Applications change every day. The pillars can't afford to.
Contact us Learn moreWhat 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.
Open systems with bug fixes
We provide open-source etcd, Apache Kafka and Apache Flink with bug fixes backed by formal TLA+ tools, and more systems are coming.
etcd
Distributed key-value store behind Kubernetes.
Apache Kafka
Event streaming platform.
Apache Flink
Stateful stream processing.
Your building block
Running on a system your business can't afford to get wrong? Talk to us.
Services
Technology and assurance services to financial entities and market infrastructures.
Formal specification
Formal specification of settlement and interoperability workflows.
Machine-checked verification
Machine-checked verification of safety and liveness guarantees, with reproducible evidence.
Counterexample analysis
Counterexample analysis in business language.
Change verification
Verification of proposed rulebook or process changes before build.
Specification and code
Methodology and tooling for keeping formal specifications synchronised with implementation code.
Formal Systems does not hold client assets, does not operate any settlement or payment system, and does not provide any financial, investment or payment service.
Get in touch
Bug fixes, formal specifications, or a conversation about trusting your foundations.
ovidiu@formalsystems.lu