What is it that a HEPA filter does? They remove airborne particles at microscopic sizes, the filter is a binary membrane. It is designed to identify and remove offending dust particles from the air. Like the air coming in from outside of a clean room even a well-designed program commonly includes tech debt and security vulnerabilities. This was a standard expectation in the early days of software development, and nothing new today.
With the recent surge of LLM integrations in coding environments and the new practice of “vibe coding” among developers, an increase in the number of vulnerabilities that can be exploited due to tech debt. LLMs routinely hallucinate answers to code no matter how good the prompts, often based on outdated code they were trained on.
Regardless of the source of a project’s tech debt, it is more and more important that technical teams thoroughly test the code base. Not only from a functional standpoint, but also to assure users that security practices are in place to prevent known attacks. Shifting left security tools reduces costly anomalies when they are identified pre-deployment. The importance of system correctness and security is paramount, especially when dealing with critical systems.
While unit tests drive white-box testing in CI/CD pipelines, adding formal verification practices to the process can have a significant impact in uncovering vulnerabilities that may not be entirely obvious at first.
What Is Formal Verification?
Within the development lifecycle, formal verification is the act of proving the correctness of a system to a formal specification or property. This is done using formal logic, set theory, and proof techniques. Think of it as turning the program into a switchboard where specific conditions are represented by "switches" that can be turned "on" or "off".
When specific switches of the switchboard (your program) are in the right order of "on" and "off", the pattern of conditions can be compared to patterns that are known to cause vulnerabilities. If they match, the formal verification program provides details of the vulnerability present. To create these switches the program is first converted into logical expression formulas referred to as Satisfiability Modulo Theories (SMT), which are a boolean representation of GOTO statements. An SMT can be thought of as the abstract form of the original byte-code. This SMT formula is then verified against verification conditions indicating a security vulnerability.
Of course when asked to add a workflow to a project the initial worry is how much additional work this will cause the technical teams. Luckily the most common tools that perform this task can be automated and integrated into existing CI/CD pipelines. Of course more daring or security-conscious users will be happy to know that open-source options for these tools support high customization adapting to the needs of the project.
Expanding Beyond Bug Hunting
Applications of these tools go beyond everyday software development. They can also be used to:
Verify adherence to network policies and architectural design requirements.
Provide verification of smart contract design and workflows, highlighting anomalies and unexpected behaviors, preventing monetary loss.
Assure that the structure of critical environments, such as healthcare or financial systems, is robust and able to handle abnormal behavior.
Let’s take a look at two examples of different uses for formal verification tools that depict how we can use them for technical projects.
A General C Example
In this example, a C program was created with intentional pointer-access issues which simulates a core issue for arbitrary code execution is analyzed using Efficient SMT-based Context-Bounded Model Checker (ESBMC).
ESBMC is a powerful formal verification tool renowned for its ability to detect and better yet prove the absence of various runtime errors in software. Developed as an SMT model checker, ESBMC targets programs written in C, C++, CUDA, CHERI, Kotlin, Python, and Solidity. Its architecture allows it to convert source code into an abstract syntax tree (AST), then into the "GOTO program" intermediate representation, which is then symbolically executed and transformed into logical SMT formulas. These formulas can be fed to off-the-shelf SMT solvers, enabling ESBMC to check for common issues like out-of-bounds array access, improper memory allocation, variable overflows, division by zero, and even concurrency issues such as data races and deadlocks. ESBMC also offers advanced verification techniques using pre-computed model checking known as Incremental Bounded Model Checking (IBMC) and a form of open ended verification called k-induction. This makes it a versatile and efficient tool for ensuring software correctness and provides improved security.
# The sample C program used in test.c
# include<bits/stdc++.h>
int main() {
// values stored in a contiguous memory block.
int arr[3] = {0,1,2};
int index = 3;
// pointer trying to access value outside the block in the next line.
int val = arr[index];
// this assertion will fail as the pointer now holds garbage val.
assert(val == 2);
return 0;
}While the error of accessing an element at an index that does not exist is trivial, this example simulates the stray pointer and memory mismanagement that often occurs in big projects. The example code when passed to ESBMC, produces the following output.
The highlighted boxes depict the input and output that contains the exact line of code that introduces a vulnerability with a counter-example that provides the misuse case. This proves that such tools can help the development team catch type mismatches and memory management issues like null pointer dereferences and double-free errors before the program is even run.
A Smart Contract Example
The next example analyzes a crypto currency contract from Ethereum, king_of_ether_throne, which was a popular ponzi scheme from way back in the initial days of Ethereum. The contract was maliciously coded so that any participant in the transaction can siphon all the money or tokens when a certain condition is met. Since the contract byte-codes are publicly available, tools like Mythril that specialize in Ethereum Solidity code analysis can be used to unearth any potential exploits in a contract, or in this case, malicious code that has been placed on purpose.
Mythril emerged in the early days of ethereum as a pioneering open-source security analysis tool specifically designed for smart contracts. Developed by ConsenSys, a leading blockchain technology company, Mythril quickly gained traction due to its ability to perform deep vulnerability analysis using techniques like symbolic execution and SMT solving on EVM byte-code. Its initial aim was to simplify the complex task of smart contract security, making formal methods more accessible to developers. Over time, it evolved as a core component of the broader MythX security analysis suite, further integrating with various development environments and solidifying its place as a crucial tool for uncovering security flaws in decentralised applications and preventing significant financial losses.
The highlighted text in the image above shows the final analysis of the given Solidity contract. Along with an explanation of the vulnerability, it also gives us the potential resource consumption of the contract in terms of estimated gas usage.
A Call For Inclusion of Cybersecurity in Software Development
CI/CD pipelines allow developers, testers, and DevOps teams to work cohesively. Including the cybersecurity team’s tools in this process can significantly benefit delivery by identifying design flaws earlier and reducing the cost of late-stage rework. In line with the “shift left” philosophy, integrating formal verification tools improves testing coverage and strengthens system resilience.
For non-technical stakeholders or product owners, formal verification may seem like an added complexity—but it’s a strategic investment. These tools offer mathematical assurance that key properties of a system hold true, reducing the likelihood of critical security issues, logic errors, or unstable behaviors making it into production. This not only minimizes long-term operational risk but also supports smoother audits, fewer hotfixes, and better trust in releases.
Beyond traditional software engineering, formal verification extends to validating configuration files, network architectures, and communication protocols with strong guarantees. While adopting these methods may require tighter collaboration between teams and slightly more design discipline up front, the payoff is a more stable, secure, and maintainable product.
Embracing advanced methodologies like formal verification adds confidence—both for engineers and for leadership—against emerging threats and the growing complexity of modern development practices.
Additional References
King Of The Ether Throne: https://www.kingoftheether.com/thrones/kingoftheether/index.html
 | A guest post by
|