I am working on a tlaplus formal verification of bitcoin. I will probably push it to delving bitcoin or the ML soon, but it's not quite ready to hit publish yet.
I'd love to get a second set of eyes or peer review though before pushing it out, so if you would like a peek dm me at thomashartman1 ( at ) gmail.
In terms of the usefulness, tldr and imho: very useful.
IMHO for bitcoin it's not so much proving things correct, as giving precise meaning to what code SHOULD do, rather than comments in english and then code that hopefully fulfills what the comment says, if the comment or code haven't drifted out of sync.
IE, tlaplus is a much better pseudocode.
Communication and clarity is the primary benefit. Proving is style point / gravy.
Also in our brand new AI world, formal and precise spec gives much better mechanisms than english handwavy prompt + some tests (probably gamed by AI) to keep the codegen from running off the rails.
Also, it is now much easier to write the specs themselves, with AI "specgen."
Hi @Scoresby or @Murch or or @justin_shocknet or anyone else interested in this stuff.
I am working on a tlaplus formal verification of bitcoin. I will probably push it to delving bitcoin or the ML soon, but it's not quite ready to hit publish yet.
I'd love to get a second set of eyes or peer review though before pushing it out, so if you would like a peek dm me at thomashartman1 ( at ) gmail.
In terms of the usefulness, tldr and imho: very useful.
https://www.youtube.com/watch?v=Fq5EQBFLEC8
"If you're not writing a program, don't use a programming language"
Leslie Lamport, 6th Heidelberg forum.
another good one is his "thinking above the code"
IMHO for bitcoin it's not so much proving things correct, as giving precise meaning to what code SHOULD do, rather than comments in english and then code that hopefully fulfills what the comment says, if the comment or code haven't drifted out of sync.
IE, tlaplus is a much better pseudocode.
Communication and clarity is the primary benefit.
Proving is style point / gravy.
Also in our brand new AI world, formal and precise spec gives much better mechanisms than english handwavy prompt + some tests (probably gamed by AI) to keep the codegen from running off the rails.
Also, it is now much easier to write the specs themselves, with AI "specgen."