An AI Approach to Verified Production Cryptographic Libraries

• URL: http://arxiv.org/abs/2608.00965v1
• Date: Sun, 02 Aug 2026 03:32:08 GMT
• Title: An AI Approach to Verified Production Cryptographic Libraries
• Abstract summary: We present CryptoProver, an AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts.<n>Without changing executable code, CryptoProver constructs a new independent proof of curve25519-dalek.
• Score: 5.564288012051712
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isolated obligations with specifications and premises already given, leaving production-library verification unresolved. We present CryptoProver, an AI-based system that synthesizes internal specifications and Verus-checked proofs from high-level API contracts. Without changing executable code, CryptoProver constructs a new independent proof of curve25519-dalek and verifies RustCrypto's previously unverified chacha20 implementation against an RFC 8439 specification. These cryptographic lineages underpin deployed systems including Signal and Shadowsocks; Signal has an estimated 218M global downloads. The independent, human-led curve25519-dalek verification was developed publicly over eight months by five main contributors. Given the API contracts and a fixed trusted library of field specifications, arithmetic facts, axioms, and vstd, CryptoProver synthesizes the internal specifications and proofs in 11.4 hours with USD 466.99 in recorded API cost. CryptoProver follows a trust-first design principle: mechanical gates reject specification weakening, invented axioms, and cross-module breakage, while isolation blocks reference proof retrieval, including from git history.

Related papers

• Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST [32.505127447635864]
  We report on the verification of memory safety for decoder components of liblzma.<n>The verification exposed undefined behavior in raw LZMA1 zero-input handling.<n>Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C.
  arXiv  Detail & Related papers  (2026-08-30T10:50:56Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• ShannonProver: Towards Automating Formal Cryptographic Proofs [14.266077895853288]
  ShannonProver is an agentic framework for automating cryptographic proofs.<n>It targets the setting in which a cryptographer provides the security model and a decomposition of the target theorem into Prov-level proof obligations.<n>We show that ShannonProver can automate substantial portions of cryptographic proof engineering for case studies.
  arXiv  Detail & Related papers  (2026-07-03T00:50:51Z)
• SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
  We introduce SecureForge, an automated pipeline that audits security risks of frontier models and produces auditing-informed secure system prompts.<n>SecureForge first identifies benign prompts that produce statically detectable vulnerabilities, and then amplifies them into a large synthetic prompt corpus of diverse scenarios.<n>On frontier models, SecureForge yields a statistically significant improvement in both unit test success and output security, with output vulnerabilities reduced by up to 48%.
  arXiv  Detail & Related papers  (2026-05-08T18:40:47Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
  arXiv  Detail & Related papers  (2026-04-29T09:57:07Z)
• GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
  Cross-chain bridges, the critical infrastructure of the multi-chain ecosystem, have become a primary target for attackers.<n>Existing defenses, such as bytecode-level static analysis, are ill-equipped to handle the semantic complexity of cross-chain interactions.<n>We propose GoAT-X, a framework that shifts automated cross-chain smart contracts auditing from pattern matching toward systematic first-principles verification.
  arXiv  Detail & Related papers  (2026-04-27T11:34:21Z)
• CryptoScope: Utilizing Large Language Models for Automated Cryptographic Logic Vulnerability Detection [10.620899430085576]
  We introduce CryptoScope, a novel framework for automated cryptographic vulnerability detection powered by Large Language Models (LLMs)<n> CryptoScope combines Chain-of-Thought (CoT) prompting with Retrieval-Augmented Generation (RAG)<n>We evaluate CryptoScope on LLM-CLVA, a benchmark of 92 cases primarily derived from real-world CVE vulnerabilities, complemented by cryptographic challenges.
  arXiv  Detail & Related papers  (2025-08-15T17:07:54Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  Large language models (LLMs) are increasingly integrated in software development.<n> Ensuring correctness in LLM-generated code remains challenging.<n>Verifiable code generation offers a promising path to address this limitation.
  arXiv  Detail & Related papers  (2025-05-29T06:12:52Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a framework that overcomes the lack of human-written snippets to enable automated proof generation of Rust code.<n> SAFE re-purposes the large number of synthesized incorrect proofs to train the self-ging capability of the fine-tuned models.<n>We achieve a 52.52% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 14.39%.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Demystifying and Detecting Cryptographic Defects in Ethereum Smart Contracts [14.203991954526789]
  We conducted the first study aimed at demystifying and detecting cryptographic defects in smart contracts. We proposed CrySol, a fuzzing-based tool to automate the detection of cryptographic defects in smart contracts. We collected a large-scale dataset containing 25,745 real-world crypto-related smart contracts and evaluated CrySol's effectiveness on it.
  arXiv  Detail & Related papers  (2024-08-09T08:40:08Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  We study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols.<n>Our measurements from the Aptos mainnet show that the optimistic approach reduces latency overhead by 71%.
  arXiv  Detail & Related papers  (2024-07-16T20:53:04Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.