pstack adds a formal verification meta-skill
pstack v0.15.27 adds /create-formal-verification-skill, a meta-skill that automatically generates a customized verification skill and a matching verification suite based on the characteristics of the system to be verified. For example, it generates a TLA+-based approach for state machines and concurrent behavior, and a Kani-based approach for Rust undefined behavior. The feature is still in beta, and the author has already found several bugs while using it to model their own code with TLA+. poteto believes that the two historical bottlenecks of modeling and spec synchronization are well suited to being taken over by LLMs, and that formal verification can give agents strong feedback that is "mathematically impossible to violate."
Topics
View original postpstack v0.15.27 ships with a new skill /create-formal-verification-skill! it's still in beta, and similar to /create-verification-skill, this is a meta-skill that creates a new skill and formal verification suite based on the characteristics you want to verify. for example, you may want to model state machines and systems with concurrency using TLA+, or use kani in rust to check for undefined behavior. if you're new to formal verification, think of it as mathematically proving properties and invariants (something that must always be true) or "laws" of your system. usually, this means modeling your programs in a separate language like with TLA+ and then running the solver on that spec. newer approaches like with kani and @bendlang take a different approach where there is no separate language: you write kani in rust, and bend in bend (it's also a programming language, and the proofs are written as laws and expressed in its type system). historically formal verification never reached mainstream status because of the difficulty in modeling and writing proofs. it's quite difficult to model your business requirements and keep them in sync! but i expect that we will see more innovation in formal verification in the future as being able to formally verifiy that the code does what you intended gives your agents superpowers in writing correct software. in the meantime though, i've been experimenting with modeling our code with TLA+ and have already found several bugs with the skill created by /create-formal-verification-skill. try it out and let me know how it goes!
View original
pstack v0.15.27 ships with a new skill /create-formal-verification-skill! it's still in beta, and similar to /create-verification-skill, this is a meta-skill that creates a new skill and formal verification suite based on the characteristics you want to verify. for example, you may want to model state machines and systems with concurrency using TLA+, or use kani in rust to check for undefined behavior. if you're new to formal verification, think of it as mathematically proving properties and invariants (something that must always be true) or "laws" of your system. usually, this means modeling your programs in a separate language like with TLA+ and then running the solver on that spec. newer approaches like with kani and @bendlang take a different approach where there is no separate language: you write kani in rust, and bend in bend (it's also a programming language, and the proofs are written as laws and expressed in its type system). historically formal verification never reached mainstream status because of the difficulty in modeling and writing proofs. it's quite difficult to model your business requirements and keep them in sync! but i expect that we will see more innovation in formal verification in the future as being able to formally verifiy that the code does what you intended gives your agents superpowers in writing correct software. in the meantime though, i've been experimenting with modeling our code with TLA+ and have already found several bugs with the skill created by /create-formal-verification-skill. try it out and let me know how it goes!
Body · AI translation
pstack has added a new skill /create-formal-verification-skill
Its positioning is as a meta-skill: it doesn't directly do formal verification for you, but instead automatically generates a customized verification skill and a matching verification suite based on the system properties you want to verify. For example, if you want to verify the correctness of state machines and concurrent behavior, it will generate a TLA+-based approach; if you want to investigate undefined behavior in Rust code, it will generate a Kani-based approach.
The concept behind it: formal verification. Testing can only prove that "bugs exist"; it cannot prove that "there are no bugs." Formal verification, by contrast, provides a mathematical proof of a system's properties: proving that some invariant (i.e., a property or "law" that must always hold true) holds in all possible cases.
poteto pointed out the distinction between two technical approaches: · The traditional approach (external modeling): use a separate specification language (such as TLA+) to model the system, then run a solver/model checker to exhaustively verify the specification over the state space. The code and the proof are two separate things. · The new approach (same-language proof): Kani is written directly in Rust, and Bend's proofs are expressed as laws in its type system; there is no separate modeling language, and the proof and the code live in the same place.
Formal verification is a field where "the theory is beautiful, but practice has never entered the mainstream." poteto pointed out two historical reasons: modeling itself is hard (abstracting business requirements into a formal model is a specialized skill), and specifications and implementations are hard to keep in sync (when requirements change, both things must be changed).
Her judgment is that these two bottlenecks happen to be what LLMs are good at taking over, letting agents bear the drudgery of modeling and synchronization. Conversely, formal verification gives agents strong feedback that traditional testing cannot provide: "mathematically impossible to violate," which is a qualitative improvement for getting AI to write correct software—she calls it a "superpower."