TLA+ model checking made symbolic
blog.acolyer.org
TLA+ model checking made symbolic
1–10 of 54 posts
Re: TLA+ model checking made symbolic
#2Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for.
I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a theory I've ever put into practise.
Re: TLA+ model checking made symbolic
#3Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
Just a nitpick: Property testing is nowhere near the level of assurance that model checking provides.
Re: TLA+ model checking made symbolic
#4Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
Amazon uses it, even made publications for it.
Re: TLA+ model checking made symbolic
#5[deleted]
Re: TLA+ model checking made symbolic
#6Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
I've come across this repo which use TLA+ to validate data migrations.
https://github.com/Shopify/ghostferry
Re: TLA+ model checking made symbolic
#7Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
iterally DDG'ing "tla industry" gets you stuff eg. https://en.wikipedia.org/wiki/TLA%2B#Industry_use.
Another 20 seconds gets you https://lamport.azurewebsites.net/tla/industrial-use.html
Re: TLA+ model checking made symbolic
#8Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
I've seen it used in RabbitMq, but I also wonder if this is used in the real world or just in academia/few technologies.
Re: TLA+ model checking made symbolic
#9Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
I reach for TLA+ any time I want to temporally model any complicated system and make sure of certain invariants, so usually any distributed system I build. The last really complicated system I used it on was to rewrite a broken message store we had implemented on top of memcached.
Re: TLA+ model checking made symbolic
#10Is anybody using TLA+ in production outside of academia? What for? I've always wanted to, but I'm not familiar enough with it to always recognize when it'd be the right tool to reach for. I primarily code in Elixir and Erlang, and have used property testing to perform some level of model checking when working with state machines, and I suspect TLA+ could be helpful for formalizing that a little bit, but it isn't a th…
I've written some models for "personal use and validation", and I keep it in my toolbelt (with Alloy) in case my thinking is not clear about something