The Proof System

Do not ask reviewers to take your mathematics on faith. Backbuild Science includes a UI-based proof system, backed by a small higher-order-logic (HOL) kernel, so the theorems and derivations behind your results are checked from first principles and travel with your paper. This page is written for readers who will interrogate exactly what the kernel checks, what a verified result does and does not guarantee, and how a proof reaches a manuscript.

The HOL kernel and the editor IDE extension are unlocked by either Backbuild Science or Backbuild Prove. Backbuild Science adds the UI-based proof system and proof entries for research, so you build and organize proofs without leaving your project. Backbuild Prove, which adds automatic in-editor diagnostics for source code and signed certificates, is a separate product and is coming soon.

Proof entries

A proof entry is a self-contained, verifiable result inside your research project: a theorem, lemma, or derivation, together with its proof. You build proof entries in the proof system's visual interface and organize them alongside the manuscript they support, so the formal argument and the written argument live in one place. Working with a proof entry has four moves:

  • State the result. Capture the claim you want to establish, as a precise formal statement.
  • Build the proof. Assemble the steps in the interface, drawing on a large library of pre-verified theorems across many mathematical domains.
  • Verify. The proof is checked against the HOL kernel. A result is either established or it is not; there is no partial credit.
  • Reference it. Cite the verified result from your manuscript so readers see exactly what has been proven, and what it rests on.

What the kernel checks, and what it trusts

The single most important thing to understand about any proof assistant is its trusted computing base: the small piece of software whose correctness you are relying on. Backbuild Science is explicit about this.

Verification is performed by a higher-order-logic kernel built on a small, auditable foundation: a handful of axioms and primitive inference rules. The kernel's only job is to check that a fully assembled proof term follows from that foundation by legitimate inference alone. Every theorem in the library is derived from the foundation through the kernel, so nothing enters the library without passing the same check.

Everything that helps you build a proof sits outside that trusted core. The visual interface, the search over existing results, and any automation that suggests steps are conveniences that assemble a candidate proof; they are not trusted to decide whether it is correct. The kernel re-checks the finished proof term regardless of how it was produced. This is the standard and deliberate design of a small-kernel system: a bug in the convenience tooling can waste your time, but it cannot make a false statement verify, because the tooling has no authority to accept a proof. Only the small kernel does.

Two nested regions. The outer dashed region, labelled Outside the trusted base, convenience not authority, holds the visual builder, search, and step suggestions, which together produce a candidate proof term. An arrow carries the candidate into a small solid inner region, the Trusted kernel, holding the axioms and primitive inference rules. The kernel outputs either verified or rejected. The caption reads: only the inner kernel decides; the helper tools can be wrong, but they can never make a wrong proof pass.
The builder, search, and suggestions only propose a proof. The small trusted kernel is the sole authority that accepts or rejects it, so a bug in the convenience tools can never let an incorrect proof through.

What "verified" actually guarantees

A verified result is a strong guarantee, but it is a precise one, and stating it precisely is part of using the system honestly:

  • It guarantees the proof is valid for the statement as written, following from the stated definitions and assumptions by legitimate inference, up to the soundness of the small kernel. There are no unverified gaps and no hand-waving.
  • It does not guarantee that your statement is the one you meant. If a definition or hypothesis is written incorrectly, the kernel will faithfully verify the wrong theorem. Verification checks the proof, not your intent, so the statement and definitions still deserve careful human reading.
  • It does not import unstated assumptions. Everything the result depends on is part of the formal statement and its cited lemmas, so a reader can see the full set of assumptions rather than trusting an informal "clearly."

In short: a verified result is correct up to its stated definitions and assumptions and the soundness of the kernel. That is exactly the assurance a careful reviewer wants, and it is far stronger than a prose proof sketch.

Proof blocks and whole-document checking in Backbuild Docs

The proof system also reaches into the manuscript itself. Backbuild Docs treats theorem, lemma, and proof environments as first-class blocks: a proof block is the document's own \begin{proof} environment, rendered as a structured card in the editor, and its mathematical obligation is what the kernel checks. Beyond checking one block at a time, a whole-document check walks every theorem-style environment in the document and returns a verdict for each one from the same higher-order-logic kernel, so after a revision you can re-check the entire manuscript in one run: each result is reported as established or rejected, so an edit that silently breaks a proof elsewhere in the document surfaces as a rejected obligation on the next check rather than going unnoticed.

Embedding a verified result in your manuscript

A proof that no one can see does not help a reader. From Backbuild Docs you can insert a proof reference: a live block that embeds an existing, verified proof entry into your manuscript. When you insert one, you pick from the proofs you have access to, and the editor confirms your access at the moment you pick, so a proof reference can only ever point at a result you are allowed to see. The reference stays linked to the proof entry, so the embedded result reflects the verified proof rather than a copied-and-pasted snapshot that can go stale. You can also insert references to a spreadsheet or a slide from the same project the same way, keeping your evidence linked rather than duplicated.

The Insert proof reference dialog open over a document in the Backbuild Docs editor. A search field labelled Search proofs by label or name is circled and captioned Search your verified proofs. The dialog is where an author picks one of their verified proof entries to cite from the manuscript.
From the document editor, Insert then Proof reference opens this picker. You search your verified proofs by label or name and drop a citation into the manuscript, so a reader sees exactly which established result the text depends on.

The shared kernel and the IDE extension

The HOL kernel is the same one that powers Backbuild Prove. In Science you use it through the visual proof system to verify the mathematics in your research; in Prove you use it to verify the correctness of source code. Either product on its own unlocks the kernel and the editor IDE extension, so a formal-methods researcher who works partly in an editor and partly in the proof UI has one consistent verification core underneath both.

Building on the Substrate corpus

You rarely start a proof from nothing. Backbuild Science subscribers can clone a read-only Substrate corpus, a large body of pre-verified results, into their own organization to build on. The clone is read-only by design, so the shared foundation stays intact. The moment you try to change something in a read-only clone, the system offers to fork it into your own editable copy, and your edits live in that fork rather than altering the shared corpus. This gives you a stable, verified base to extend while keeping your own work cleanly separated. Access to clone and fork is part of the Science subscription and is enforced per action.

Why it matters for research

Catch errors early

A flawed lemma is caught when you write it, not after a referee finds it, or worse, after publication.

Machine-checked rigor

Verified results give reviewers machine-checked assurance that your derivations hold, with the full set of assumptions visible, rather than a prose sketch.

Reproducible

Proof entries are part of your project. They can be re-checked and can be referenced from the paper, so the formal results travel with the work.

Pairs with your writing

The proof system works hand in hand with the research editors: state and prove a result in the proof system, then reference it from your LaTeX manuscript in Docs. When you export the manuscript and share your project, the verified proofs are part of the same project, so the formal argument and the paper stay together.

Frequently asked questions

What exactly does the kernel check versus trust?
The small kernel type-checks the finished proof term against a handful of axioms and primitive inference rules. The visual builder, search, and any step suggestions are outside the trusted base: they assemble a candidate, but only the kernel decides whether it is correct.
What does "verified" actually guarantee?
That the proof is valid for the statement as written, following from the stated definitions and assumptions, up to the soundness of the kernel. It does not guarantee your statement says what you intended, so definitions and hypotheses still deserve careful reading.
Can I put a verified result into my paper?
Yes. From Backbuild Docs, insert a proof reference to embed a verified proof entry as a live, access-checked block that stays linked to the proof rather than a stale copy.
Is this the same kernel as Backbuild Prove?
Yes. The same HOL kernel underlies both; Science uses it to verify mathematics through the proof UI, and Prove uses it to verify source code. Either product unlocks the kernel and the IDE extension.
Do I have to build every theorem from scratch?
No. You draw on a large library of pre-verified theorems, and you can clone a read-only Substrate corpus into your organization and fork it into an editable copy to extend.