Thinking Hard is not Enough
summary
Claim: thinking hard alone fails for complex blockchains, so a spec-first workflow pairs formal specs with executable checks. Quint uses temporal-logic-style semantics, lightweight simulation and model checking (TLC and fast simulators) to find concrete counterexamples — for example it discovers a sequence that yields an account balance of -1. Quint then emits Quint-generated tests that bind spec to implementation and turn the squiggly spec→code arrow into a straight, test-backed guarantee; about 100 early users are already collaborating.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:06Reliable distributed systems in 2025
- 3:56Code aligns teams better than specs
- 6:48Spec-driven development problems
- 8:57Blockchain systems need precise specs
- 10:21Introducing Quint
- 12:26Quint in modern software engineering
- 14:13Future of software engineering
related talks
30mAsk the expert - Thinking Mathematically Above The Code Level
21mMaking Concurrent Hardware Verification Sequential
57mResearch on Different Time Horizons (and an Example with Machine-Checked Proofs)
48mThe Verification of a Distributed System
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
38mDealing With Complexity in the Blockchain and Beyond
20mSift: Using Refinement-guided Automation to Verify Complex Distributed Systems
19mFormally Verifying Optimizations with Block Simulations