Algebraic Verification vs Smart Contract Testing
Test suites check specific inputs and assert expected outputs. Algebraic verification proves that declared invariants hold over all possible inputs and all reachable state sequences. These are fundamentally different coverage models. Testing is probabilistic. Verification is mathematical. They are complementary, not competing.
How Smart Contract Testing Works
Smart contract testing uses three primary approaches: unit tests, integration tests, and fuzz testing. Unit tests check individual functions with predetermined inputs and expected outputs. Integration tests exercise sequences of transactions to verify multi-step behavior. Fuzz testing generates random or semi-random inputs to discover edge cases that manually written tests miss.
Test coverage is measured as the percentage of code paths exercised by the test suite. A contract with 90% line coverage still has 10% of its code untested. A contract with 100% line coverage may still miss state-dependent bugs that only appear after specific sequences of transactions.
Fuzz testing improves coverage significantly over manual test writing. Tools like Echidna and Foundry's fuzzer can run millions of random inputs against invariant properties. However, even millions of inputs are a negligible fraction of the total input space for contracts with 256-bit integer state. Fuzz testing finds bugs efficiently, but it cannot prove their absence.
How Algebraic Verification Works
In Formagine, invariants are declared as part of the form definition. The compiler extracts a proof obligation for every (transition, invariant) pair and discharges each one algebraically. If a transition preserves an invariant for all possible inputs and all reachable predecessor states, the proof succeeds. If not, the compiler produces a counterexample.
This is not sampling. The compiler does not test a single input. It proves over the entire domain. For a conservation invariant like sum(balance) == supply, the compiler verifies that every transition preserves this identity by algebraic manipulation, regardless of the specific values of balance, supply, or the amount transferred.
The result is a binary guarantee: either the invariant holds for all possible executions, or the form does not compile. There is no concept of coverage percentage because coverage is total for declared invariants.
Key Differences
| Dimension | Testing | Algebraic Verification |
|---|---|---|
| Coverage model | Probabilistic (specific inputs) | Mathematical (all possible inputs) |
| Guarantee | Bug found or not found | Property holds or counterexample produced |
| State sequences | Tests specific transaction sequences | Proves over all reachable state sequences |
| Maintenance | Tests must be updated when code changes | Invariants re-verified automatically on compilation |
| Execution cost | Minutes to hours (fuzz campaigns) | Seconds (part of compilation) |
| Expressiveness | Can test any observable behavior | Limited to compiler-supported invariant classes |
| Edge cases | Must be anticipated or discovered by fuzzer | All edge cases covered by universal proof |
| Integration | Can test cross-contract interactions | Verifies single-form invariants only |
| Setup cost | Test harness, mock contracts, test data | Declare invariants in the form definition |
Testing Approaches in Detail
Unit testing
Unit tests check individual transition functions with specific inputs. A transfer test might verify that sending 100 tokens from Alice to Bob updates both balances correctly. The test passes for these specific values but says nothing about what happens with different amounts, addresses, or initial states.
Integration testing
Integration tests exercise transaction sequences: deploy the contract, mint tokens, transfer between accounts, attempt an unauthorized burn, and verify the final state. These tests are valuable for verifying expected workflows but can only test the sequences the developer writes.
Fuzz testing
Fuzz testing generates random inputs and checks that invariant properties are not violated. This is the testing approach closest to verification in spirit. A fuzzer running for hours might test millions of input combinations. However, the state space of a typical smart contract with multiple 256-bit variables is astronomically larger than any feasible sample. Fuzz testing finds bugs with high probability but cannot prove their absence.
Property-based fuzzing (as in Echidna or Foundry) defines invariants and then searches for violations. The invariants look similar to Formagine's invariant declarations. The difference is in the verification method: fuzzing searches stochastically while algebraic verification proves symbolically.
Limitations of Algebraic Verification
Algebraic verification proves what you declare. If you forget to declare an important invariant, the compiler has no reason to check it. Testing, by contrast, can catch surprising behavior even without a formal specification, because the developer observes the output and notices when something is wrong.
Algebraic verification operates on a single form in isolation. It does not test integration with frontend code, wallet interactions, or cross-contract message flows. These remain the domain of integration testing.
The invariant classes supported by the compiler are powerful but bounded. Some properties are difficult or impossible to express in the current invariant language. For these, testing remains the practical verification approach.
Limitations of Testing
Testing can never prove the absence of bugs. A passing test suite means no bug was found in the tested inputs, not that no bug exists. This is a fundamental limitation, not a practical one. Dijkstra's observation that "testing shows the presence of bugs, never their absence" applies directly to smart contract security.
Test maintenance is a real ongoing cost. As contracts evolve, tests must be updated, new edge cases must be anticipated, and test infrastructure must be maintained. For complex contracts, the test suite can grow larger than the contract itself.
Test flakiness, environment-dependent failures, and incomplete mocking of external dependencies introduce noise that can mask real issues or create false alarms. The signal-to-noise ratio of a test suite degrades over time without active maintenance.
When to Use Each
Use algebraic verification when your contract has critical state invariants that must hold universally, such as conservation laws, access control rules, or bounds constraints. Algebraic verification provides mathematical certainty for these properties with no ongoing maintenance cost.
Use testing when you need to verify user-facing behavior, integration with external systems, or properties that are difficult to express as algebraic invariants. Tests remain the best tool for catching unexpected behavior that no formal specification anticipated.
Use both as a default practice. Algebraic verification eliminates an entire category of bugs (invariant violations) from your testing burden, allowing your test suite to focus on business logic, user experience, and system integration. The two approaches cover different failure modes and are stronger together than either is alone.
Frequently Asked Questions
- Can algebraic verification replace smart contract testing?
- For declared invariants, yes. If a property is expressed as an invariant and the form compiles, that property holds for all possible inputs and state sequences. However, testing catches behavior you did not think to declare. Tests for user-facing logic, integration, and unexpected behavior remain valuable.
- Is fuzz testing equivalent to algebraic verification?
- No. Fuzz testing generates random inputs and searches for violations, which improves coverage over manual tests but remains probabilistic. Algebraic verification proves over all possible inputs. The difference is between high statistical confidence and mathematical certainty. They complement each other because fuzz testing can check properties that are hard to express algebraically.
- What is the maintenance cost of algebraic verification vs test suites?
- Test suites require ongoing maintenance when contract logic changes. Algebraic verification has no separate maintenance burden because invariants are part of the form definition. When you change a transition, the compiler automatically re-verifies all invariants. There is no test file to update.
- Should I still write tests if I use algebraic verification?
- Yes, for properties outside the invariant system. Algebraic verification proves declared invariants, but it does not test user-facing behavior, frontend integration, or cross-contract interaction patterns. The difference is that you no longer need tests to verify invariant properties, because those are mathematically guaranteed.