Understanding Formal Verification and Testing

Although formal verification has a rich history of over 70 years, it remains a niche field, practiced by only a small group of researchers and engineers. One reason for this is the general lack of awareness about formal methods. Another reason, in my opinion, is the confusion between testing-based verification and formal verification. I've often found myself explaining how my role as a formal verification engineer differs from testing. This is my humble attempt to clarify the distinction between formal verification and testing for a layman.

<aside> 🔥

There's a common misconception that formal verification is equivalent to exhaustive enumeration (i.e., testing every possible input or state of a system). While both concepts aim to ensure correctness, they are fundamentally different in approach and scope. Exhaustive enumeration involves testing every possible input, state, or scenario in a system to verify its correctness. It is often impractical for complex systems because the number of possible inputs or states can be astronomically large (or even infinite). Exhaustive enumeration is typically limited to very small systems or components where the input space is manageable. Formal Verification does not rely on testing specific inputs or states but instead reasons about the system's behavior abstractly. It creates a formal model (e.g., using logic, automata, or mathematical representations) and the model is checked via formal methods such as model checking or theorem proving.

</aside>

Aspect Formal Verification Testing
Definition Formal verification is a process that uses mathematical methods to prove or disprove the correctness of a system's design with respect to a certain formal specification or property. Testing-based verification is a process that involves executing the actual system or software under controlled conditions to observe its behavior and outputs. The goal is to detect errors, bugs, or deviations from the expected results by running specific test cases.
Approach Mathematical Proof: Uses mathematical techniques to prove correctness with respect to a formal specification.
Exhaustive Analysis: Aims to cover all possible states and behaviors of the system, providing a complete guarantee that the system adheres to its specifications under all possible conditions. Empirical Execution: Executes the system with specific inputs and observes outputs or behavior.
Sampling Based: Testing is inherently incomplete because it only checks a subset of all possible inputs and scenarios. It can not guarantee the absence of errors in untested cases.
Scope • Exhaustive Coverage: Examines all possible behaviors within the formal model.
• Focus on Correctness: It is particularly useful for verifying critical properties such as safety (e.g., "the system will never enter a dangerous state") and liveness (e.g., "the system will eventually reach a desired state"). • Partial Coverage: Limited to specific test cases and scenarios. It cannot explore all possible states or inputs, especially in complex systems.
• Focus on Functionality: Testing is more practical for verifying functional requirements and ensuring the system works as expected in typical use cases.
Guarantees • Absolute Guarantees: If a system is formally verified, it provides a mathematical proof that the system will behave as specified under all possible conditions. This is particularly valuable for safety-critical systems (e.g., aerospace, medical devices, or autonomous vehicles).
• No False Negatives: If the verification passes, there are no hidden bugs or edge cases that could cause failures. • Relative Guarantees: Testing can only provide confidence based on the quality and coverage of the test cases. It cannot guarantee the absence of bugs in untested scenarios.
• False Negatives Possible: Even if testing passes, there may still be undiscovered bugs in the system.
**Complexity
and Effort** • High Complexity: Formal verification requires expertise in formal methods, mathematical modeling, and logic. It can be time-consuming and computationally expensive, especially for large or complex systems.
• Scalability Challenges: It may struggle with scalability for very large systems due to the state explosion problem (e.g., in model checking). • Lower Complexity: Testing is generally easier to implement and understand, as it involves executing the system and observing results.
• Scalable but Incomplete: Testing can be scaled to larger systems by adding more test cases, but it remains inherently incomplete.
Applicability • Critical Systems: Used in safety-critical or mission-critical systems where absolute correctness is required (e.g., avionics, nuclear control systems, cryptographic protocols).
• Hardware Verification: Commonly used in hardware design (e.g., verifying microprocessors or circuits). • Non-Critical Systems: Suitable for systems where absolute correctness is not required, or where the cost of formal verification is prohibitive.
Outcome Provides a proof of correctness or identifies specific violations of the formal specification. Provides evidence of correctness for the tested scenarios but cannot prove the absence of errors.
Limitations Limited by system complexity and feasibility of formal modeling. Limited by test coverage; cannot guarantee absence of bugs in untested cases.

Testing versus Formal Verification with Examples

Let's walk through two simple examples of how testing is performed both in software and in hardware.

Software Example

Let’s take an example where both testing-based verification and formal verification can be applied. We'll use a Python function for illustration, but the principles apply to any programming language.

Example: A Function to Check if a Number is Prime

We’ll use a function that checks whether a given integer is a prime number. A prime number is a natural number greater than 1 that has no positive divisors other than 1 and itself.

Function to Verify

Here’s a Python function to check if a number is prime:

def is_prime(n):
    if n <= 1:
        return False
    for i in range(2, int(n**0.5) + 1):
        if n % i == 0:
            return False
    return True

Testing-Based Verification

Testing involves running the function with specific inputs and checking if the output matches the expected result.