Stop Guessing. Start Proving. Formal Verification with Halmos

x.com/shanzson
x.com/zokyo_io
x.com/opensensepw

Tests are nice, but what if you could prove your contract won’t break?

In this session, we fire up Halmos and go all in, from setup to writing specs, catching real bugs, and tearing through the DStable vault backdoor. No fluff. Just raw code, broken invariants, and receipts.

It focuses only on real execution paths and finds bugs your tests can’t even reach.

Timestamps
00:00:03 Why formal verification actually matters
00:00:26 What fuzzers miss — and Halmos doesn't
00:01:56 Installing the CLI & getting started
00:02:24 Writing your first spec with setup()
00:04:06 Loop constraints and cheat-codes
00:06:53 Sender/receiver conditions in specs
00:08:07 Basic preconditions and invariants
00:10:30 Filtering inputs with require
00:12:01 Handling arrays & edge cases
00:14:00 Avoiding noise in results
00:17:25 How Halmos narrows down execution paths
00:20:38 First full spec run
00:22:32 Dealing with reverts & assumptions
00:23:59 Overview of the built-in example suite
00:28:25 Finding and understanding your first bug
00:29:46 How Halmos picks counter-examples
00:34:06 Making counter-examples more readable
00:37:42 Building a low-level encoder spec
00:41:10 Macros and typed variable tricks
00:49:14 Another bug found — live
00:55:42 Kicking off the next example
00:57:25 Deep dive into the vault contract
00:59:17 Testing internal balances
01:02:08 Spotting a major logic flaw
01:05:13 Invariants that track over time
01:07:08 Testing those invariants in practice
01:11:29 Vault: backdoor breakdown
01:12:46 Writing a spec to catch the exploit
01:17:00 A bigger spec setup from scratch
01:21:35 Running the full test suite
01:25:32 Digging into the final bug
01:28:45 Best practices + common mistakes
01:30:04 Reviewing everything we used
01:31:10 Wrap-up & where to go next