# How to Write Formally Verifiable Specifications in Python

**Summary:** We can write specifications that are formally verifiable without needing to move away from Python and the benefits that come with it. In this session, we will explore how this can be done.

**Facilitator:** Roberto Saltini

**Note Taker:** TBD

**Pre-Reads:**
- [Draft 3SF Specification Documentation](https://github.com/saltiniroberto/ssf/tree/separate_bft/high_level/README.md)
- [ethresear.ch post on 3SF](https://ethresear.ch/t/3-slot-finality-ssf-is-not-about-single-slot/20927)

**[Draft Slides](https://docs.google.com/presentation/d/1xtKPqN9KnMnIZfbl-7A7C7L9-ynJKVlpmmtD4UfMVtQ)**

## Agenda

- Presentation
- Pitfalls in the way the current specification are written and how to avoid it
- Walk through a practical example: [the draft 3SF specification](https://github.com/saltiniroberto/ssf/tree/separate_bft/high_level/README.md)
- Open Discussion
- Is the resulting spec readable enough?
- How can we improve readability without sacrificing formal verifiability
- Alternative approaches

## Notes & Action Items

*Breakout sessions will **not** be recorded.*

*Good notes will help everyone who could not be in the room get up to speed on what happened. Unless instructed otherwise by a participant, please default to using [Chatham House Rules](https://en.wikipedia.org/wiki/Chatham_House_Rule#the_rule).*

*This will make the process easier, but in cases where there is value in specifying a specific individual (e.g. they are championing a proposal, taking on an action item, etc.), you can mention them. Similarly, nothing should be "off the record", but if someone is uncomfortable with a statement being part of the notes, please respect this.*

*As a calibration point, see the [ACD recaps](https://ethereum-magicians.org/t/all-core-devs-execution-acde-198-october-10-2024/21314/2?u=timbeiko)*