TYPED: The Formal Verification Roundtable
This is a call to those who no longer accept “it probably works” as evidence.
Curated by the TYPED team.
KaizenLabs × CryptoLar present
Brazil’s inaugural closed-door forum for formal verification and protocol safety.
What Is TYPED
TYPED is a one-day technical event focused on formal methods & security, from a beach house in Floripa because it's Brazilian summer 😎
More than talks, this is an opportunity to bring together our top-notch talent to exchange valuable knowledge and network. But sure we have talks!
Formal Specs-Driven Development by coproduto @ cumbuca.com, how a real company integrates formal specifications into their engineering workflow.
Sharing & Optimality by: EduardoRFS, hardcore functional programming fundamentals.
Quint specifications guiding LLMs by: Gabriela Moreira & Erick Pintor @ Informal Systems, hear from the creator of Quint herself how to leverage formal specs for your AI development workflow
Formally Verifying zkVMs by: Fabrício @ Nethermind — formal approaches to proving properties in cryptographic systems
Backtesting Cryptography: Active F/OSS contributing and maintaining cryptography libraries, Lucas Oliveira
Verificação ZKP: Lean and Clean, Christiano Braga @ UFF
Between talks, expect open discussions, whiteboard sessions, and the kind of technical conversations that don't happen at typical conferences. Plus Brazilian BBQ, good coffee, and beer.
What You Can Expect
TYPED takes place as a full-day technical retreat at Founder Haus, Florianópolis.
Participants rotate through small-group and one-on-one sessions across the day, with continuous open discussion and problem solving.
You can expect:
• A curated group of protocol and security engineers
• Structured table sessions focused on formal verification and invariants
• Direct review of real systems, specifications, and proofs
• Whiteboard problem solving and design critique
• A full Brazilian BBQ lunch prepared on-site
• Unlimited coffee and flavored water throughout the day
• Kombucha on tap and draft beer
• Comfortable indoor and outdoor spaces for quiet discussion
This is not a passive schedule.
It is a continuous working table from morning until evening.
Who Should Attend
TYPED is designed for engineers and researchers interested in protocol safety and formal verification at any stage of their journey, from active practitioners to motivated newcomers ready to learn deeply.
This forum is intended for:
• Formal verification engineers
• Smart-contract auditors
• Protocol and infrastructure developers
• ZK and cryptography researchers
• Engineers working with specifications, invariants, or mathematical modeling
Participants should be comfortable discussing:
• Smart-contract architecture and protocol design
• Formal methods, specifications, or invariant reasoning
• Code and mathematical models in small-group settings
This event is designed to connect you directly with engineers working on the hardest problems today, and the methods being used to solve them.
Engineers early in their journey are welcome, as long as they are prepared to engage seriously.
You do not need to be an expert to participate.
Curiosity, preparation, and willingness to listen matter more than seniority.
Why Formal Verification
Code correctness always mattered, business just prioritized distribution. With AI this suddenly becomes even worse because now even the devs which were the bastions of technical excellence, are faced with the choice of giving up on code quality and tapping into Coding Agents, or doing things the old way and getting behind on the curve.
That's a false dichotomy. We always had the solution, it was just too hard for most programmers, and it's not anymore: Formal Methods.
Formal Methods are the pinnacle of programming for humans, dependently-typed languages could be described as the most annoying compiler ever. But for machines it turns coding into a supervised problem, the compiler is their friend, giving them granular feedback.
And on the other hand with have blockchain. As it scales and gets more adoption and liquidity, that money turns into involuntary bug bounties. We've seen what North Korean hackers can do. Bugs are an existential issue for the blockchain.
And together with blockchain comes Programmable Cryptography, such as Zero-Knowledge, where every code becomes math, and any math mistake means everything goes south.
Testing finds bugs.
Audits catch issues.
But only formal verification can prove entire classes of failure cannot exist.
TYPED exists to accelerate the practical adoption of mathematical verification in real-world protocol engineering.
Day Flow
• 13:30 Arrival, setup, coffee & warm-up conversations
• 14:00 Talks start
• 16:00 Brazilian BBQ dinner, informal whiteboarding & rotating sessions
• 18:00 – 22:00 Wind-down sessions with light electronic music, drinks, swag handout & open networking
Your Hosts
TYPED is curated by founding teams actively building at the intersection of protocol security, research, developer and founder education.
A group of real people hosting something serious.
Supported By
CryptoLar
A grassroots builder movement dedicated to high-signal Web3 education, security research, and developer networking across Brazil and LATAM.
https://x.com/CryptoLarBrasil
KaizenLabs
A research-driven engineering collective focused on applied security, formal methods, and verification-first development practices.
Founder Haus
A physical home for founders and deep-tech builders in Florianópolis, providing the space where real collaboration, experimentation, and high-trust technical exchange can happen.
Nethermind Security
A world-class blockchain security practice delivering audits, formal verification, and advanced protocol research, supporting leading Web3 teams with battle-tested engineering expertise and rigorous security methodologies.
https://x.com/nethermindsec
Zokyo
Zokyo is a leading Web3 security firm providing end-to-end audits for smart contracts, protocols, wallets, and digital infrastructure. Operating across EVM, Solana, Cosmos, and Move ecosystems, with expertise in Solidity, Rust, and Go, Zokyo delivers advanced testing, fuzzing, threat modeling, and economic analysis through its Econ Lab to help teams build secure, resilient, and compliant blockchain products.
https://x.com/zokyo_io