Hello,

As we continue to push the envelope (no pun intended) on applying formal verification to a web dev workflow, one thing is becoming clear: flexibility must be baked into the system.

Formal verification has traditionally been used where correctness is rigid — security, blockchain, critical systems. But for web apps, flexibility is an essential feature of user experience. When a user's literal request can't be fulfilled, the system should still try to achieve their intended goal.

That's the concept of completeness: not rejecting valid actions. You could write property tests to check whether an action should be accepted, but that requires enumerating all potential candidates and sampling over an infinite state space. 

In our system, to verify completeness, you define an intent envelope that defines which interpretations of a request preserve the user's intent. This isn't done via sampling various scenarios; it's written as a predicate.

In this new post, we discuss the concept of completeness vs soundness and how proofs handle completeness in ways that are difficult for property tests.

We have appreciated all the engagement and feedback so far. If you have questions or thoughts you’d like to share, please hit reply.

~fernanda

Github | LinkedIn