Does anyone have resources that talk about writing a TLA+ model for an existing ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		_cairn on Jan 20, 2020 \| parent \| context \| favorite \| on: How Amazon Web Services Uses Formal Methods (2015)... Does anyone have resources that talk about writing a TLA+ model for an existing software system as opposed to designing a new system using TLA+ as the design reference?

lemmster on Jan 20, 2020 | [–]

Below are a few specs related to refactoring/rewriting the TLA+ model checker to scale to more cores:

* https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...

* https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...

* https://github.com/lemmy/PageQueue

hwayne on Jan 20, 2020 | [–]

Check out Marianne Bellotti's work. She recently gave a talk at Strange Loop on writing specifications of existing systems: https://www.youtube.com/watch?v=oMSmkRGzQ64

_cairn on Jan 21, 2020 | [–]

Thank you! I will check this out.

Consider applying for YC's Summer 2026 batch! Applications are open till May 4
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact