Jan  

#Quint, a language built on top of #TLA+ to make formal specifications more accessible.

https://quint.sh/

Crazy that #LLM coding will make formal verification mainstream in the next 2 - 3 years.

#FormalVerification #TLAPlus #Testing #ModelChecking #Concurrency #Prediction

Quint, an executable specification language for reliable systems

Quint is an executable specification language. Write specs you can run, simulate, and verify, so subtle bugs get caught before reaching production.

May 27 at 12:26pmWeb
Show threadMikalaiMay 27

@janriemer
Thinking about it as Large Language Condensates, not models, leads to
- formal languages have structure, that can be captured by condensation that keeps pattern's essence
- one would expect a result in formal things. Why surprise?

#llm #llc

Show threadJan  May 27

@mikalai I think we have a misunderstanding here:

Sure, LLMs can help writing proofs, but that's not the (main) reason why formal verification will become more and more popular, IMHO.

Formal verification will become more popular, because the software industry will try to counter-balance the increasing defect rate caused by LLM code output.