CSLib: Building a Platform for AI-assisted Formal Verification in Lean

Submitted by Katie Dey on
 AI is revolutionizing the way code is written, but with more and more AI-generated code, the dangers of AI-introduced bugs and vulnerabilities are also increasing. At the same time, AI has also dramatically increased the capabilities of malicious actors, making even existing code more vulnerable. Fortunately, there is hope. The same GenAI power also shows promise in helping write formal specifications and in creating proofs, thus lowering the bar for formal verification. This leads naturally to a vision of a future in which AI only generates fully verified code.

AI as an Enabler for Analyzing Business Logic Systems

Submitted by Katie Dey on

Business Processes and Business Logic (BL) systems that govern and operationalize these processes are critical to both the US economy as well as the DoD mission. Logic faults in these systems have the potential to severely impact production of essential products or impede procurement of critical parts and services. For instance, a mismatch between a part tolerance in a manufacturing specification and the implementation of that specification in a manufacturing plan can cause numerous downstream effects, including shipment delays, recalls, or failures.

Transitioning Assurance Case Technology to Production—an Experience Report

Transitioning Assurance Case Technology to Production—an Experience Report

The software certification and approval process has long been a challenge in the
development lifecycle. Recently, under the auspices of DARPA, Lockheed Martin began
introducing technology poised to revolutionize the software approval process. This new
solution called ArcCert, starts at program inception and automates many of the manual,
tedious tasks involved in gathering and curating artifacts for presentation to certification
authorities. By making certification-relevant artifacts available throughout the entire

Submitted by Gerilynn Pearce on

Marktoberdorf Summer School 2026: Engineering Secure and Dependable Software Systems

Marktoberdorf Summer School 2026: Engineering Secure and Dependable Software Systems

Applications are now open for the 2026 Marktoberdorf Summer School, a premier international program focused on engineering secure and dependable software systems.

Organized by fortiss and the Department of Informatics at Technische Universität München, and led by Peter Müller (ETH Zurich) and Alexander Pretschner (TU München, fortiss, bidt), the program brings together leading researchers and students to explore state-of-the-art approaches to building software systems that are both safe and secure.

Submitted by Katie Dey on
Subscribe to