Workshop
Interactive symbolic testing with TLA+, Apalache, and LLMs
—
Page · Talks & lectures
Talks & lectures
Invited talks, conference presentations, workshops, and tutorials on TLA+, Apalache, Quint, and the protocols they check.
18 listed
Year
Kind
Title
Venue
Material
Video
Invited talk
Symbolic search and test generation with Apalache & LLMs
—
Workshop
Hands-on symbolic search & test generation with Apalache
—
Talk
How model checking can help build trust in distributed protocols like Single Slot Finality
—
Panel
Formal verification in the Ethereum Protocol: current status and future directions
—
Talk
Specification and model-checking of the ZKsync Governance Protocol
—
Talk
Pragmatic bounded model checking for TLA+ with Apalache
—
—
Tutorial
Apalache Tutorial
—
Workshop
Finding bugs for fun & profit with Informal Systems
—
—
Lectures
Quint, TLA+, and Apalache
—
—
Talk
Quint
—
Tutorial
Apalache: symbolic model checker for TLA+
—
Talk
How TLA+ and Apalache helped us design the Tendermint Light Client
—
—
Talk
Model-based testing with TLA+ and Apalache
—
Talk
Type inference for TLA+ in Apalache
—
Talk
Formal spec and model checking of the Tendermint Blockchain Synchronization Protocol
—
Tutorial
Parameterized verification with Byzantine Model Checker
—
Tutorial
Apalache for TLA+
—
More talks are listed in the CV.