The Fundamental Principles behind Our Verification Platform

7 min read Original article ↗

At Predictable Machines, our mission is creating tools that help build trust around systems. For these trust-building tools to be truly reliable, they must deliver trustworthy results themselves. Trustworthy results = trustworthy systems. Of course!

What is "trustworthiness"?

But wait, what does that mean? A system can be said to be trustworthy if the information you get from it reflects reality in an honest way. For example, imagine a car navigation system that tells you to take some path, but that path is blocked to traffic. The system gave you a confident answer that didn't reflect reality. That's an untrustworthy result, which leads to a loss of trust in the navigation system. Next time you have to rely on a navigation system, you will think twice about using this particular one.

However, the navigation system could still have suggested going through that path if it were convinced it was the best route, but also warned the user about the possibility of it being blocked. What this accomplishes is empowering the user with enough information so that they can make their decision on what path to follow. Systems often cannot be absolute truth oracles, but by conveying information honestly, they become trustworthy.

With AI, this matters now more than ever

The challenge of trust in software has always existed, but AI code assistants have amplified it dramatically. Tools Claude Code, OpenAI Codex, and GitHub Copilot are now helping developers produce code at a pace that is orders of magnitude faster than what we could accomplish a couple years ago. This is incredibly powerful, but it creates a new problem: more code is being produced faster than it can be sustainably reviewed.

AI-generated code can be confidently wrong in subtle ways, like in our navigation system example. A model might produce a function that looks correct, passes a few tests, and reads well; but silently mishandles an edge case or misinterprets the intended behavior. The more code you generate this way, the more these risks compound. Software verification has always been important, but in a world where AI assistants can generate entire projects within minutes, it becomes essential.

Our fundamental principles (of trustworthy verification)

Predictable Code, our first product, aims to help build trust in software by providing a software verification platform supporting a wide variety of programming languages. The verification platform at the core of Predictable Code leverages a mix of precise techniques (such as theorem proving) and approximate techniques (such as large language models).

In the context of software verification, the same definition of trustworthiness that we described before holds. A software verification system is reliable and trustworthy not when it provides correctness results with absolute confidence, but when it has the power to honestly report back what assumptions, approximations, and potential limitations it found during the verification process that could compromise the verification results. This, again, empowers users to make their own decisions based on these results: sometimes users might be fine with not having absolute confidence in whether certain areas of a piece of software are correct. Other times, there could be some other areas where correctness is non-negotiable: think of critical systems.

This is why we landed on the following fundamental principles that light the path for all the design decisions we make when developing Predictable Code to make sure it is a reliable and trustworthy tool for software verification:

  • When performing verification of pure code (with no side effects), the verification framework will try to model the semantics of the program being verified. When it is infeasible for the verification framework to model some of the semantics precisely, the approximations taken must be made explicit in the verification results.
  • When performing verification of code with unknown side effects or side effects that cannot be confidently modeled by the verification framework, it must be explicit about the assumptions it is making with regard to those side effects in order to give clear verification results (e.g. if it assumes that a call to an effectful function within the program being verified succeeds, it must state that fact in the verification results or in the function's contract).
  • When performing verification of code with well-understood side effects whose behavior can be confidently modeled by the verification framework, as is the case with pure code, the verification framework will try to model the semantics of the side effects involved in the program being verified. When it is infeasible for the verification framework to model some of the semantics precisely, the approximations taken must be made explicit in the verification results.
  • The verification framework should not confidently yield false positives: if a program is not correct, the verification result should never assure the user that the program is correct.
  • The verification framework should not confidently yield false negatives: if a program is correct, the verification result should never assure the user that the program is not correct.
  • To prevent confident false positives and false negatives, the verification framework must express any uncertainties and alert the user in its output when it was unable to reliably guarantee a program's correctness.

What do trustworthy reports look like in practice?

Picture this scenario: we ask a verification platform to verify a function that reads from a database, applies some logic to the data, and returns a result. However, while this system is able to verify the function's core logic, it cannot fully model the database interaction.

In this scenario, a not-so-trustworthy verification system might report:

✅ Verification result: function adheres to its specification.

But a more trustworthy/transparent system following might report something like this instead:

✅ Verification result: function adheres to its specification.
⚠️ Assumption: database query returns a valid result.
️⚠️ The function might not behave as expected when the database query fails.

The second output does not imply "less correctness" because it contains warnings. It is simply more expressive: it tells you exactly where your confidence holds and where it doesn't. This empowers you to decide whether those assumptions are acceptable for your use case, or whether you need to double check them to ensure your desired level of trust in your software.

Establishing a feedback loop

There is an added benefit to all of this besides making our platform trustworthy. We stated previously that honest answers empower users to make decisions. But we can also leverage those decisions to improve the verification process. For instance, when there are several possible ways to approach the verification of a given piece of software, the platform can ask the user to choose between the possible strategies to accomplish verification results that more accurately reflect their intention. This in turn increases the level of trust they can place in those results. A powerful, positive feedback loop.

Trust, but verify

Having said all that, it is virtually impossible to find a system that is perfectly trustworthy. Users of verification platforms should be encouraged to go with a "trust, but verify" mindset when using them: always double-check results, and pay close attention to assumptions, especially ones that might not be obvious or that could be hidden!

This applies doubly when working with AI-generated code. AI code assistants are fantastic productivity tools, but they shift the development burden from writing code to verifying it. Our goal with Predictable Code is to make that verification step as reliable and transparent as possible, so that you can confidently adopt AI-assisted development without sacrificing trust and reliability in your software.

Follow along

If this reflects what you're seeing in modern software development, you can leave your email to follow the project as it evolves.

👉 Join the updates. 2026 will be a formative year for Predictable Code.