Supported Languages

Backbuild Prove verifies pf2 annotations across 20+ programming languages. The same proof format works everywhere; only the comment syntax differs. The launch language set is grouped by category below, with specialized domains (Solidity, CUDA/OpenCL, advanced SQL) available as add-ons.

After this page you will know whether your stack is covered, which comment syntax to use, how many languages your plan includes, and what is available as an add-on.

Backbuild Prove is launching soon. The language set, tiers, and add-ons below are the launch plan. See the pricing page for current plans and any add-on pricing.

Launch Language Set

All of the following are part of the launch language set. They use the same pf2 annotation format with language-appropriate comment syntax; only the comment delimiters differ.

Systems & Native

Language File Extensions Comment Syntax
Rust.rs/// ... or /* ... */
C.c, .h/* ... */
C++.cpp, .hpp, .cc, .cxx, .hxx, .hh/* ... */
Objective-C.m, .mm/* ... */ or // ...
Go.go/* ... */
Swift.swift/* ... */
Ada.ada, .adb, .ads-- ... (line prefix)

Web & Application

Language File Extensions Comment Syntax
TypeScript.ts, .tsx, .mts, .cts/** ... */
JavaScript.js, .jsx, .mjs, .cjs/** ... */
Python.py, .pyi# ... (line prefix)
Dart.dart/// ... or /* ... */

Enterprise & JVM

Language File Extensions Comment Syntax
Java.java/** ... */ (Javadoc)
Kotlin.kt, .kts/** ... */ (KDoc)
C#.cs/* ... */

Functional & Data

Language File Extensions Comment Syntax
Haskell.hs, .lhs{- ... -} or -- ...
SQL.sql, .psql, .plsql, .tsql-- ... (line prefix)
Lua.lua-- ... (line prefix)

Low-Level

Language File Extensions Comment Syntax
x86_64 Assembly (GAS / AT&T).s, .S# ... (line prefix)
x86_64 Assembly (NASM).asm; ... (line prefix)
ARM64 Assembly.s, .S// ... or /* ... */
WebAssembly.wat, .wast;; ... (line prefix)

Specialized Add-ons

Some domains are available as specialized add-ons on top of your plan’s proof languages. They use the same pf2 format and verification pipeline. See the pricing page for add-on details.

Add-on File Extensions Comment Syntax
SQL (advanced compliance).sql-- ... (line prefix)
Solidity.sol/** ... */ or // ...
CUDA.cu, .cuh/* ... */
OpenCL.cl/* ... */

Tier Limits

The number of proof languages included in your subscription depends on your plan tier. See the pricing page for current plans and any add-on details.

Plan Included Languages
Pro 2 languages
Team 4 languages
Business 10 languages
Enterprise All languages included

Add-on: SQL Verification

SQL verification is available as a separate add-on with tier-specific pricing. SQL annotations verify stored procedures, queries, and schema constraints using the same pf2 format. See the pricing page for current add-on details.

Enterprise SQL includes formal proof printouts suitable for compliance audits. These machine-verified documents provide evidence for:

  • PCI DSS: data access control and query integrity
  • SOC 2: logical access controls over data
  • ISO 27001: information access restriction
  • HIPAA: access control and audit controls

Language-Specific Examples

Rust

Rust uses doc comments (///) or block comments (/* ... */). Place the annotation directly above the function: 

/// prove:pf2("max_returns_larger")
/// \[
/// \begin{pre}
///   a : \mathbb{N} \land b : \mathbb{N}
/// \end{pre}
/// \begin{proof}
/// \step{1}{ a \geq b \Rightarrow \text{result} = a }
///   \pf\ By first branch.
/// \step{2}{ a < b \Rightarrow \text{result} = b }
///   \pf\ By second branch.
/// \step{3}{ \text{result} \geq a
///   \land \text{result} \geq b }
///   \pf\ By \stepref{1} and \stepref{2}.
/// \qedstep
///   \pf\ By \stepref{3}.
/// \end{proof}
/// \]
fn max_of(a: u64, b: u64) -> u64 {
    if a >= b { a } else { b }
}

TypeScript

TypeScript uses JSDoc-style block comments. The annotation works in both .ts and .tsx files: 

/** prove:pf2("clamp_bounded")
\[
\begin{pre}
  \text{min} \leq \text{max}
\end{pre}
\begin{proof}
\step{1}{ v < \text{min}
  \Rightarrow \text{result} = \text{min} }
  \pf\ By Math.max branch.
\step{2}{ v > \text{max}
  \Rightarrow \text{result} = \text{max} }
  \pf\ By Math.min branch.
\step{3}{ \text{min} \leq \text{result}
  \leq \text{max} }
  \pf\ By \stepref{1} and \stepref{2}.
\qedstep
  \pf\ By \stepref{3}.
\end{proof}
\]
*/
function clamp(v: number, min: number, max: number): number {
  return Math.min(Math.max(v, min), max);
}

Python

Python uses # line comments. Place the annotation on consecutive comment lines directly above the function: 

# prove:pf2("factorial_positive")
# \[
# \begin{pre}
#   n : \mathbb{N}
# \end{pre}
# \begin{proof}
# \step{1}{ \text{factorial}(0) = 1 > 0 }
#   \pf\ By base case.
# \step{2}{ \text{factorial}(n) > 0
#   \Rightarrow \text{factorial}(n+1)
#   = (n+1) \cdot \text{factorial}(n) > 0 }
#   \pf\ By inductive step: product of positives is positive.
# \qedstep
#   \pf\ By induction, \stepref{1} and \stepref{2}.
# \end{proof}
# \]
def factorial(n: int) -> int:
    if n == 0:
        return 1
    return n * factorial(n - 1)

Is my stack covered?
The launch set above spans systems and native, web and application, enterprise and JVM, functional and data, and low-level languages, all using the same pf2 format. Every listed language shares one proof format and one kernel; only the comment syntax changes. Specialized domains (Solidity, CUDA/OpenCL, advanced SQL) are add-ons.

How many languages do I get, and can I change them?
Pro includes 2 proof languages, Team 4, Business 10, and Enterprise all of them. On Pro and Team, swapping an included language slot is subject to a 30-day cooldown; adding a language as a paid add-on has no cooldown. See the pricing page.

What if a specific construct in my language cannot be translated?
You cite that boundary as an explicit assumption in the annotation and prove everything built on it; the kernel still checks those steps. This is the same escape hatch described under Documenting External Dependencies.

Next Steps