AI for Bug Detection using Formal Methods
Module 3 Code to Documentation
Project Lead Dr Kashif Saghar/ Adnan Elahi
Institution CESAT, Islamabad
Report Date: 23/09/2025
Report Status: Module 3 code to document completed
Executive Summary
This paper presents a secure, offline AI-driven formal verification module that converts insights
from prior debugging and testing stages into mathematically provable correctness contracts.
Leveraging Ollama (local LLM orchestration), Mistral-7B (NLP reasoning), and Frama-C for static
analysis, the system automatically generates ACSL annotations and pre/post-conditions from
low-level requirements (LLRs) and testing insights. By integrating AI parsing with formal
methods, the module delivers certified bug-free code blocks for embedded and defense-grade
systems. Operating entirely on-premises, it meets NESCOM’s strict data privacy standards while
reducing manual annotation effort and improving verification accuracy.
Ensuring mathematically proven correctness in embedded and defense-grade software is
essential, as undetected defects can result in mission failure, severe financial loss, or security
breaches. Embedded systems in aerospace and defense environments often operate under
strict real-time constraints, interact closely with hardware, and function in unpredictable
conditions. Even minor bugs can cascade into critical failures.
While Modules 1 and 2 provide powerful tools for AI-assisted debugging and automated test
generation, these approaches primarily identify and address defects at a practical level—they
do not guarantee formal mathematical correctness. Achieving provable assurance requires
formal methods, which rigorously validate that the software behaves exactly as specified under
all conditions.
Existing tools such as Frama-C and SPARK/Ada are industry-proven for formal verification but
demand detailed annotations and contracts (preconditions, postconditions, and invariants).
Deriving these contracts manually from informal specifications or test cases is time-consuming,
error-prone, and requires specialized expertise.
To address this challenge, Module 3 introduces an AI-driven approach that integrates Ollama-
hosted Mistral models to automatically infer formal contracts. By parsing low-level
requirements (LLRs), debugger insights, and test outputs from previous modules, the system
generates ACSL annotations and verification-ready contracts. This workflow not only reduces
manual effort but also accelerates verification without compromising accuracy or security.
Furthermore, the system operates entirely offline, ensuring NESCOM’s privacy and data-
protection mandates are upheld. By bridging AI capabilities with formal verification techniques,
this module strengthens the overall development pipeline—transforming debugging and testing
outputs into certified, bug-free code blocks suitable for mission-critical applications.
The AI for Bug Detection Using Formal Methods module serves as the bridge between AI-
assisted debugging/testing (Modules 1 and 2) and mathematically proven software verification.
Its purpose is to transform insights and artifacts—such as low-level requirements (LLRs),
debugger logs, and generated test cases—into formal verification (FV) contracts that can be
processed by tools like Frama-C or SPARK/Ada.
At a high level, the system’s architecture consists of the following components:
Input Layer Collects outputs from Modules 1 and 2, including parsed code insights,
annotated test cases, and LLR documents.
NLP Contract Inference Engine (Mistral via Ollama) Processes specifications, logs, and
test data to infer preconditions, postconditions, and loop invariants.
Frama-C / SPARK Verification Backend Uses the generated ACSL annotations to
perform static analysis and formal verification, identifying unproven assertions or
potential bugs.
IDE Integration Layer Presents verification results, certified code blocks, and
unresolved issues to developers within a familiar IDE-like interface.
Workflow of Operation:
1. Data Collection Gather LLRs, test results, and debugger logs from prior modules.
2. Contract Inference Use Mistral (hosted locally by Ollama) to derive formal contracts
and ACSL annotations.
3. Formal Verification Execute Frama-C or SPARK/Ada to validate the code against the
inferred contracts.
4. Result Presentation Display verified code blocks, warnings, or failed assertions within
the IDE for developer action.
This modular and offline-secure design ensures that sensitive defense code never leaves the
local environment, while offering flexibility to upgrade models or integrate additional
verification backends in the future.
FUNCTIONAL REQUIREMENTS
The AI for Bug Detection Using Formal Methods module shall meet the following functional
requirements to ensure rigorous, secure, and efficient verification of embedded and defense
software:
1. Input Aggregation and Preprocessing
o Collect and parse outputs from Modules 1 and 2, including LLRs, debugger logs,
and test case reports.
o Normalize data formats for consistent handling by the NLP engine.
2. NLP-Driven Contract Inference
o Use Mistral (via Ollama) to analyze requirements and test results.
o Automatically generate preconditions, postconditions, and loop invariants for
C/C++ code functions.
o Infer missing details from incomplete or ambiguous specifications where
possible.
3. ACSL Annotation Generation
o Produce Frama-C compatible ACSL contracts for each identified code block.
o Support contract customization and human-in-the-loop review before formal
analysis.
4. Formal Verification Execution
o Invoke Frama-C (or SPARK/Ada when applicable) to perform static analysis and
formal verification.
o Detect potential bugs, unverified properties, and unsafe operations.
5. Bug Certification and Reporting
o Present verified, certified bug-free code blocks in an IDE-like environment.
o Generate verification logs, structured reports (JSON, XML, or CSV), and
annotated code for audits or downstream use.
6. Integration with Downstream Tools
o Provide APIs or export functions to integrate verified outputs with Simulink
heuristics or additional verification workflows.
NON-FUNCTIONAL REQUIREMENTS
Category Requirement
Performance The system shall complete contract generation and formal verification for
medium-sized functions (<500 LOC) within ≤3 seconds on a mid-range
GPU/CPU, ensuring responsiveness in iterative development cycles.
Security All code, logs, and verification processes shall run locally with no external
API calls, ensuring NESCOM-level confidentiality and compliance with
defense security policies.
Scalability The backend shall use a modular, service-oriented architecture, allowing
integration of alternative AI models, additional verification tools, or
expanded codebases without major redesign.
Usability The interface shall offer clear visualization of verified/unverified code
paths, easy navigation of annotations, and inline explanations of
verification results to reduce developer effort and learning curve.
Maintainabilit Deployment shall be containerized (e.g., Docker) for easy installation,
y upgrades, and rollback, with well-documented code and configuration for
long-term support and future enhancements.
Reliability The system shall provide ≥99% uptime under controlled conditions and
gracefully handle verification failures, logging all issues for audit and
debugging.
Portability The module shall run on both Linux and Windows environments with
minimal configuration changes, ensuring compatibility with varied
development setups.
TOOLS AND METHODS
Tool Role in the System Key Advantages
Ollama 3.x Local orchestration server to host and • Fully offline, ensuring
manage Mistral models for NLP-based NESCOM-level security.
contract inference. • Easy deployment via
Docker or native installers.
• Flexible architecture to
swap or upgrade models
without redesign.
Mistral-7B Core NLP model used to parse LLRs, • Optimized for code
debugger insights, and test outputs to reasoning and natural
generate pre/post-conditions and loop language understanding.
invariants. • Open-source and
lightweight—runs on modest
hardware.
• Fine-tunable for domain-
specific rules (e.g., ACSL
syntax).
Frama-C Formal verification tool for C code, using • Industry-standard static
ACSL annotations to prove correctness. analysis and formal
verification framework.
• Supports multiple plug-ins
for advanced analyses.
• Free and widely adopted in
safety-critical domains.
SPARK/Ada Alternative backend for Ada or mixed- • Strong formal guarantees
(optional) language projects requiring high-assurance for high-integrity systems.
verification. • Complements Frama-C for
projects using Ada or mixed
languages.
Docker Containerization platform for deployment • Simplifies installation and
and consistency across environments. scaling.
• Ensures reproducible builds
and easy maintenance.
• Cross-platform
compatibility.
COMPARISON: PAID VS FREE SETUPS
Aspect Paid Tools (e.g., MathWorks Free / Open-Source Tools (e.g.,
Polyspace, CodeSonar, AdaCore Ollama + Mistral-7B, Frama-C,
SPARK Pro) SPARK/Ada Community, Docker)
Integration & Offers seamless IDE integration, Requires manual configuration and
UX premium support, and polished tuning; interface may be less polished
user interfaces with minimal setup. but remains functional for
development workflows.
Performance Backed by enterprise-grade Dependent on local hardware
infrastructure with optimized resources; may require tuning or
solvers—fast verification even on incremental verification for very large
large codebases. projects.
Data Privacy May require transmitting metadata Fully offline processing ensures
or using license servers—potential NESCOM-level confidentiality with no
risks for defense-grade projects. external data transfer.
Cost High one-time licenses or recurring Zero recurring cost—free and open-
subscription fees—significant source tools eliminate licensing fees
ongoing expenses for enterprise and reduce long-term operational
environments. cost.
Customization Vendor-controlled features with Fully modifiable—contracts,
limited flexibility for project- heuristics, and model behavior can be
specific adaptations or customized or extended to meet
experimental heuristics. specific verification needs.
Long-Term Risk of vendor lock-in—loss of Complete independence and control
Control functionality if subscriptions lapse —no reliance on third-party vendors
or policies change. for critical verification tasks.
EXPECTED OUTCOME
The implementation of Module 3: AI for Bug Detection Using Formal Methods is expected to
deliver the following outcomes:
1. Certified Bug-Free Code Blocks
o Source code verified against formally generated ACSL contracts, ensuring
mathematical correctness.
o Confidence that the code meets safety and performance standards required for
defense and embedded applications.
2. Automated Annotation Workflow
o Significant reduction in manual effort for writing preconditions, postconditions,
and invariants.
o Faster onboarding for developers unfamiliar with formal specification languages
like ACSL.
3. Improved Verification Accuracy
o AI-driven contract generation reduces human oversight errors.
o Early detection of potential issues prevents costly fixes later in the development
cycle.
4. Seamless Integration with Existing Pipelines
o Outputs (certified code blocks, verification logs) are fully compatible with
Simulink heuristics, formal verification tools, and audit workflows.
o Easy export in JSON, XML, or CSV formats for downstream processes.
5. Enhanced Security and Compliance
o All processing occurs locally, ensuring NESCOM’s strict confidentiality standards
are upheld.
o Eliminates reliance on external cloud services, mitigating risks of data leaks.
6. Scalable and Future-Ready Framework
o Supports the addition of more advanced models or verification backends.
o Lays the foundation for scaling to system-level verification and complex model-
based design.
The AI for Bug Detection Using Formal Methods module establishes a critical bridge between AI-
assisted debugging/testing and mathematically guaranteed correctness for defense and
embedded software. By integrating Ollama-hosted Mistral models with formal verification tools
like Frama-C and SPARK/Ada, the system transforms low-level requirements, debugger outputs,
and test results into precise ACSL contracts and formally verified code.
This approach eliminates the need for manual annotation—a traditionally time-intensive and
error-prone task—while maintaining offline operation to satisfy NESCOM’s strict security and
privacy standards. The module ensures that software is not only tested but proven correct,
reducing the likelihood of undetected bugs in mission-critical environments.
Furthermore, its modular and scalable architecture allows future integration of larger AI
models, additional verification frameworks, and advanced heuristics. By embedding formal
verification directly into the AI-driven development workflow, this module strengthens
NESCOM’s overall assurance pipeline—delivering certified, bug-free code blocks that are ready
for integration with Simulink heuristics and higher-level system verification tasks.
This combination of AI and formal methods represents a cost-effective, secure, and forward-
looking solution for maintaining the reliability, safety, and compliance of critical defense
software.