Testing, QA and Software Verification
Independent verification for software that cannot afford to be wrong — on any stack, in any language.
Most testing tells you the cases you thought of still pass. We work on the ones you didn’t think of: what the system is supposed to do, written down precisely, and then checked against what it actually does.
What we work on
Your test suite. What it covers, what it silently doesn’t, and which of its passes are load-bearing. A suite that is green and thin is worse than no suite, because it buys false confidence.
Your specification. Most codebases don’t have one. Where none exists we derive it from the implementation and confirm it with your team — and the act of writing it down is routinely where the first real defects surface, before a line of test code is written.
The properties that must always hold. Balances that must never go negative, state machines that must never reach two states at once, invariants that survive every ordering of events. These are the things example-based tests are worst at and property-based testing is best at.
AI-generated code. Increasingly some or all of a codebase is written by an LLM. That code is plausible but not necessarily correct — it compiles, it reads well, and it can be subtly wrong in ways review does not catch. The methods on this page are the ones that do catch it. Tell us what was generated and we will scrutinise it accordingly.
Building on Cardano? Cardano smart contract audits → are the specific case of this work.
How we verify
We pick the lightest method that will actually settle the question. Proof is expensive and is not always the right answer; the skill is knowing which parts of a system earn it.
Specification. Stating precisely what the system must do, in a form that can be checked rather than argued about. Everything else depends on this, which is why it comes first.
Property-based testing. Instead of asserting one example, we state a property that must hold for every input, and let the machine hunt for the counterexample. When it finds one it shrinks it to the smallest failing case, which is usually the difference between a bug you can fix in an hour and one you argue about for a week.
Test suite review and reinforcement. We read your existing suite for coverage and for the omissions that matter, then extend it. Whatever we find, you keep — the tests stay in your repository and run in your CI after we’re gone.
Formal methods, where they earn their cost. For the parts of a system where being wrong is unrecoverable, properties can be proved rather than sampled. We have applied this to a consensus algorithm and to a stablecoin’s economic invariants — the two kinds of system where a subtle error is not recoverable after launch. Most codebases have a small number of places that justify this and a large number that do not, and saying which is which is part of the job.
Manual review against the specification. Code read by a person who knows what it is supposed to do, looking for the gap between the two. Automation is good at the errors it has been told to look for; this is for the rest.
What you get
A written specification of what your system is supposed to do — often the first one that has existed, and useful long after we’ve finished.
A findings report, every issue by severity, each with a recommendation to fix or mitigate. You get a draft first, so you can respond and counter-argue before anything is final.
Tests that stay yours. Every defect we find is demonstrated by a test, and that test becomes part of your suite. No unreproducible findings, and no severity ratings you have to take on faith.
A re-check after your fixes land, confirming the fixes work and that nothing new was introduced.
A written account of what we could not verify and why. The limits of an engagement are part of its result; a report that implies total coverage is not worth having.
How we scope it
Verification work is sized by how much has to be true, not by how many files there are. A large, repetitive codebase with a handful of real invariants can be quicker than a small one where everything is load-bearing.
So we scope by reading, not by counting. We look at what the system does, which parts would be unrecoverable if they were wrong, and what already exists to build on — then we come back with a fixed price and a span for the work that is actually warranted.
That means the conversation comes first, and it is a real one: we would rather tell you that a two-week review is enough than sell you a proof you don’t need.
What we need from you
A conversation, so we understand what the system is for and what “wrong” would cost you.
A mutual NDA, in place before we read anything that isn’t already public.
Someone who can answer questions. The specification phase generates them, and the answers are usually where the interesting problems are.
A build we can run, and whatever tests exist today, however incomplete.
Why MLabs
We have verified systems outside Cardano. MLabs formally verified GRANDPA, the consensus algorithm behind Polkadot — a protocol where an error is not something you patch after the fact. We also reverse-engineered and re-implemented the payments system at Juspay, which is a different discipline from verification but the same underlying demand: understand precisely what a system does before trusting it with money.
We have verified while building, not just from the outside. On DJED, MLabs built features and carried out the formal verification of the system it was building on. Verification integrated into delivery catches design errors while they are still cheap to change; an arms-length audit at the end can only report them.
We maintain the tools other people verify with. Plutarch, Lambda Buffers and CTL are MLabs projects, used across the Cardano ecosystem. Maintaining infrastructure that other teams depend on is a different discipline from consuming it, and it is where this practice came from.
Correctness is the house specialism, not a service line we added. MLabs is a Haskell and formal-methods consultancy. The techniques on this page — specification, property-based testing, reasoning about invariants — are how the team works by default, not a methodology adopted for an engagement.
Find out what it would take
Tell us what you’re building and what it would cost you to be wrong. We’ll tell you which parts are worth verifying, which aren’t, and what that would involve — before anyone looks at code, and under a mutual NDA when we do.