#Formal-Verification
5 posts in tag “Formal-Verification”.
The Curry-Howard Correspondence: How Type Theory Bridges Proof and Computation
2025-03-18Explore the profound isomorphism between logical proofs and computer programs: how the Curry-Howard correspondence unifies propositional logic with typed lambda calculus, and how it enables modern proof assistants like Coq, Lean, and Agda.
CHERI and Capability Hardware: Memory Safety at the Gate Level
2025-03-11How CHERI Concentrate compression, the load barrier for temporal safety, and the Arm Morello prototype are reshaping what it means to build a secure processor — and why formal verification of capability integrity is the hard part.
Smart Contract Security: Reentrancy, Front-Running, and Verification with Certora and Foundry
2023-09-15A rigorous treatment of smart contract vulnerabilities—reentrancy, integer overflow, front-running/sandwich attacks—and the modern verification toolkit including the Certora Prover and Foundry fuzzing framework.
Formal Verification of Cryptographic Protocols: ProVerif, Tamarin, and the TLS 1.3 Verification Story
2023-04-06An exploration of the Dolev-Yao model, ProVerif and Tamarin provers, computational soundness results, and how formal methods proved TLS 1.3 secure before deployment.
Abstract Interpretation: The Cousot Framework, Galois Connections, and Sound Static Analysis by Construction
2022-01-20A rigorous exploration of abstract interpretation—Patrick and Radhia Cousot's unifying framework for static program analysis, from Galois connections to widening operators and the soundness proofs that guarantee analysis correctness.