Resources
Browse a collection of resources designed to help you build safer, more secure software. Explore real-world case studies, technical guides, books, and the latest updates from the AdaCore blog.
Latest Blog Posts
Johannes Kanig
Rotate, Sort, Last Column: The Burrows Wheeler Transform in SPARK
See how AI proved full functional correctness for classical and bijective Burrows-Wheeler Transforms in SPARK.
M. Anthony Aiello
Foundational Cryptography in SPARK
See how AI wrote and proved SPARK Platinum code for AES, SHA-256 and HMAC from the NSA’s Cryptol…
Ghjuvan Lacambre
Try Taint Analysis in CodeSonar for Ada
Learn how Taint Analysis in CodeSonar for Ada finds SQL injection and other critical security flaws…
Tom Bosque-Jehier
Proving Kruskal’s Algorithm in SPARK: When Generative AI Meets Formal Verification
Can Generative AI prove SPARK code? Testing Claude on formal verification of Kruskal’s MST…
Case Studies
How Stoneridge, Inc. Enhances Vehicle Safety with CodeSonar®
CodeSonar helps Stoneridge to achieve the safety and security that they need, efficiently allowing engineers to spend more time developing new and…
NASA Study Explores the Benefits of Static Analysis
NASA operates the Space Network, a mission-critical satellite telecommunications system that requires continuous, uninterrupted service. To improve…
Starting Left: How eLeapPower Supports Continuous Innovation with Static Analysis
eLeapPower is an automotive technology company that develops advanced electric powertrain and charging systems for electric vehicles. To help meet…
