5 papers
An AI Approach to Verified Production Cryptographic Libraries
Chuyue Sun, Su Fong, Zhiyi Kuang +5
Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isola…
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi +5
We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs…
ClassInvGen: Class Invariant Synthesis using Large Language Models
Chuyue Sun, Viraj Agashe, Saikat Chakraborty +5
Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not on…
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Leni Aniva, Chuyue Sun, Brando Miranda +2
Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a sur…
Clover: Closed-Loop Verifiable Code Generation
Chuyue Sun, Ying Sheng, Oded Padon +1
The use of large language models for code generation is a rapidly growing trend in software development. However, without effective methods for ensuring the correctness of generate…