Troubleshooting

Solutions for common issues encountered when using Backbuild Prove. Each section covers the symptoms, cause, and fix.

After this page you will be able to diagnose and resolve the most common verification problems: connection and authentication errors, missing annotations, timeouts, language gating, signing-key issues, cross-check failures, and unexpected cache behavior.

Backbuild Prove is launching soon. If you hit an issue not covered here once it is live, reach us through the contact page.

Connection Failed

Symptoms: The CLI reports a connection error when running backbuild prove run or other commands that contact the Backbuild API.

Causes and fixes:

  • Network connectivity: verify you have internet access and can reach api.backbuild.ai.
  • Authentication expired: run backbuild auth status to check your authentication state. If expired, run backbuild auth login to re-authenticate.
  • Firewall or proxy: ensure your network allows outbound HTTPS connections to api.backbuild.ai on port 443.

No Annotations Found

Symptoms: The scanner completes but reports zero annotations, even though your code contains prove:pf2 markers.

Causes and fixes:

  • Wrong file extensions: verify that the files containing annotations have extensions matching the configured languages. For example, TypeScript annotations must be in .ts or .tsx files.
  • Wrong comment syntax: each language requires its own comment style. Python uses # line comments (Python has no block comments, and """...""" are string literals, not comments). Rust uses // or /* ... */. See the annotations reference for the correct syntax per language.
  • Exclude patterns: check your .backbuild-cli/prove.json project settings for exclude_patterns that might be filtering out the directories containing annotations.
  • Language not enabled: confirm the language is included in your subscription or added as an add-on. Check your enabled languages at subscription settings.

Verification Timeout

Symptoms: Verification runs exceed the configured timeout and are terminated before completion.

Causes and fixes:

  • Increase timeout: set a higher timeout_ms value in your .backbuild-cli/prove.json project settings, or pass backbuild prove settings --timeout <ms>. Complex proofs with many steps may need more time.
  • Reduce parallelism: lower the max_parallel setting. Fewer concurrent verifications reduce memory pressure and can allow individual proofs to complete faster.
  • Simplify proof steps: break large proofs into smaller lemmas. A proof with many steps requires more kernel time than several smaller proofs that build on each other.

Language Not Allowed

Symptoms: The scanner skips files for a specific language with a “language not allowed” message.

Causes and fixes:

  • Check subscription tier: Pro plans include 2 languages, Team plans include 4, and Business plans include 10. Enterprise plans include all languages. Verify your tier at subscription settings.
  • Check language selections: in the project settings, confirm the language is in your selected set or added as an extra language add-on.

Language Swap Cooldown

Symptoms: Attempting to swap an included language returns a cooldown error.

Cause: Pro and Team plans enforce a 30-day cooldown between language swaps on included language slots. If you swapped a language within the last 30 days, you must wait for the cooldown to expire.

Fix: Either wait for the cooldown period to expire, or add the language as a paid add-on, which has no cooldown restriction. See the pricing page for current add-on details.

LSP Server Not Found

Symptoms: The VS Code extension reports that it cannot find or start the Backbuild Prove language server.

Causes and fixes:

  • Language server unavailable: the VS Code extension runs the bbprove-lsp language server, which it bundles or downloads automatically on first use. If the download failed, retry from the extension’s error notification or follow the getting started guide.
  • Custom binary path: if you installed bbprove-lsp in a non-standard location, set the backbuild.lspBinaryPath setting in the VS Code extension configuration to the full path of the bbprove-lsp binary.
  • Verification falls back to the CLI: if the bbprove-lsp binary is unavailable, the extension verifies via the backbuild-cli instead. Ensure the backbuild binary is installed and on your system PATH, then restart VS Code.

Signing Key Issues

Symptoms: Verification or certification commands fail with signing key errors.

Causes and fixes:

  • Key file permissions: signing keys in ~/.backbuild/bbprove-keys/ must have restrictive permissions. On Unix systems, set permissions to 0600 (owner read/write only): 
    chmod 0600 ~/.backbuild/bbprove-keys/*
  • Missing key files: if no signing key has been registered yet, backbuild prove publish generates and registers one automatically on its next run. If the server already has an active key but its private key file is missing from ~/.backbuild/bbprove-keys/, copy the key from the machine that registered it, or revoke the key and let the next publish register a fresh one.
  • Key rotation: after a key rotation, the private key for the new active key lives on the machine where the rotation was performed. Publishing from another machine requires copying that private key into ~/.backbuild/bbprove-keys/.

Lean 4 Cross-Check Failures

Symptoms: Proofs pass the HOL kernel but fail the Lean 4 cross-check step.

Causes and fixes:

  • Kernel export differences: the HOL kernel’s exports may use constructs or encodings that differ from what Lean 4 expects. Review the specific error message for which term or type caused the mismatch.
  • Type variable leaks: ensure proof steps do not introduce unbound type variables that the Lean 4 translator cannot resolve.
  • Contact support: persistent Lean 4 cross-check failures may indicate a translator bug. File an issue with the full error output.

Parser Skip

Symptoms: Certain functions are reported as parser_skip in the issues list and are not verified.

Cause: The language parser cannot translate certain code constructs into the kernel’s term language. Common cases include inline assembly, FFI calls, macros, reflective code, and complex metaprogramming.

Fix: For functions containing untranslatable constructs, document the untranslatable portion as an explicit assumption in the \begin{doc} section of your annotation and reason about it in your proof steps. This preserves soundness while making the dependency explicit and auditable. See Documenting External Dependencies in the annotations guide.

Cache Returning Stale Results

Symptoms: Verification returns cached results even though you believe the annotation has changed.

Cause: Backbuild Prove uses a content hash of the annotation to determine whether re-verification is needed. If the annotation content is unchanged (including whitespace within the proof), the cached result is returned.

Fix: Any change to the annotation content triggers re-verification. If you changed only the code body (not the annotation), the cache is still valid because the annotation itself did not change. To force re-verification, make a change inside the annotation (even adding a space to a comment line) and run again.

Next Steps