SecGPT

We will explore the use of LLMs (Large Language Models) in conjunction with formal methods. Our work will focus on safety critical programs written in the programming language Rust for which we will use finetuned LLMs to audit Rust programs and assist in formal verification of cryptographic code and other security critical applications. Concretely, the project will proceed in two tracks: 1. Exploration of an AI powered automatic code reviewer, focusing on security and vulnerability checking. 2. Translation of security specifications in natural language into formal specifications using LLMs for the verification of Rust code