Reliability, Specification, and a New Paradigm of Development

Formal methods have long been a beautiful, effective but expensive technique for building and analyzing software. AI coding agents are making them cheap. Proofs that once took years of expert work can now be produced by agents and checked by machine.

What remains is a human task. Someone has to decide whether the specification says what we actually mean, and to answer for that decision. We believe this is where the work of building reliable software and mathematics is moving, away from writing the implementation and toward understanding the specification.

We build three things for this shift. The auditable vouching record makes reliability concrete by recording who has checked which part of a specification, so that confidence can be quantified in a fine-grained way. A refinement calculus of specifications connects the rigor of formal language with the readability and flexibility of natural language. Together they lead to a new way of developing, in which the specification is the language everybody works in.

Reliability and the auditable vouching record

The reliability of intellectual artifacts, such as software and mathematical proofs, decomposes into two parts. One is whether the artifact is a correct implementation of some specification, and the other is whether the specification is aligned with human intention. It is much easier nowadays to check the implementation in a proof assistant like Lean, and AI coding agents now enable formal proofs far larger than was previously possible. In recent results, AI agents have completed a Lean formalization of Fermat’s Last Theorem,¹ and have proved key security properties of Signal’s core cryptographic protocol.²

This makes checking the specification even more important, because we want to be sure that what we implemented or proved is what we actually wanted. The issue has already surfaced in a recent release of AI-generated proofs of open mathematical problems.³ Mathematicians objected that the results came without understanding,⁴ and the lab behind the release has since committed funding to help mathematicians examine and understand them.⁵

Checking the specification has become the bottleneck in making an artifact reliable. This step is surprisingly hard: people have to make the leap from their internal mental model to external code. This is where understanding comes from, and we need a system that supports this process.

We interpret reliability as a chain of trust. In formal verification with Lean, reliability rests on trust in the hardware, the compilers, the implementation of the proof assistant, and the encoding of the statement. For the general public, confidence rests on trust in domain experts. Their vouching carries weight because they answer for it. This is why formal verification still needs humans in the loop, at least until AI agents can take responsibility as well.

Building on this, our way to improve reliability is the auditable vouching record. An auditable vouching record breaks the encoded Lean statement down into the basic concepts it is built from. Together these form what we call the Trusted Specification Base (TSB). It then records, for each concept in the TSB, the judgment of domain experts on whether its encoding is aligned with human intention. In this way the leap from mental model to code is taken incrementally, and the record itself serves as evidence of reliability. It quantifies how much confidence we have, instead of giving only a yes or no. Also, the implicit intentions of a group of people sometimes diverge, and working through the record helps them reach consensus.

A modern spec design

The auditable vouching record provides the collaborative structure for reliability. The design of the specification language, in turn, determines whether the methodology can be widely adopted. The traditional choice is formal logic, such as Lean code. Formulas use symbols and logical connectives to state a property rigorously, so that it can be machine-checked. But they are hard to read and inaccessible to engineers without a background in logic, and they are often domain-specific and do not generalize. AI coding agents, on the other hand, take free natural language as the specification. Natural language is far more readable and flexible, but it has its own drawbacks: a specification can be ambiguous, redundant, and even inconsistent.

Designing a specification language is essentially a trade-off between rigor and flexibility. To bring formal verification out of the ivory tower, we build a refinement calculus of specifications. We observe that natural language can be seen as an ambiguous abstraction of formal logic, and that it is the right level for most users to work at. Refining a specification means elaborating a natural-language description into formal logic, step by step ruling out ambiguity and approaching machine-checkable code. This process connects natural language to formal logic, and it can happen interactively and incrementally.

Spec-oriented development

With the auditable vouching record and a refinement calculus of specifications, we can verify the reliability of an existing artifact. Combined with AI coding agents, the same method points to a new paradigm of specification-oriented development, in which the specification is worked on while the artifact is being developed. Users describe their intention in natural language, then interactively refine the spec until it is concrete enough. Throughout the refinement, agents build the artifact automatically and verify it in the corresponding logic, achieving correctness by construction.

Developers already talk to their agents in natural language to develop artifacts, but the practice is still implicit and unstructured. By analogy, the specification is the new programming language, and AI agents are powerful compilers. A specification refined in our calculus is then a good candidate for the “source code” of AI agents.

We see a future in which developers, engineers and product managers can leave implementation details behind, collaborate on the specification, and obtain verified, highly reliable artifacts. We build the product and the workflow that make this paradigm practical.