Draft:Proofware
Formally verified software
From Wikipedia, the free encyclopedia
Proofware is a category of software design where the primary deliverable is a system of formally verified proofs that establish a trustworthy boundary between intent and side effects.[1] In this architecture, the boundary functions as a deterministic checker that accepts or rejects actions based on machine-checkable constraints, serving as the sole writer to the application state.[2]
 | Review waiting, please be patient.
This may take 8 weeks or more, since drafts are reviewed in no specific order. There are 2,950 pending submissions waiting for review.
Where to get help
How to improve a draft
You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Editor resources
Reviewer tools
|
Conceptually, proofware contrasts with terms like vaporware or shimware. While vaporware describes software that fails to ship, and shimware describes software that ships without strengthening invariants, proofware describes software where formally verified constraints are the primary product.[1]
Properties
Proofware is characterized by five functional properties derived from principles of trustworthy computing:[1]
- Formally verified: boundary invariants are proven rather than merely tested. A proof guarantees a property holds for all inputs, distinct from the sampling approach of standard testing.[3]
- Deterministic: given the same state and the same action, the checker consistently produces the same accept or reject decision, a requirement for predictable state machine replication.[4]
- Traceable rejection: every rejection includes a deterministic reason trail. The checker explains the violation rather than silently dropping the action, similar to the generation of counterexamples in model checking.[5]
- Sole writer: application state is only modified through the boundary. No side channel is permitted to bypass the checker, enforcing the principle of complete mediation found in reference monitors.[6]
- Interface-agnostic: the boundary verifies the validity of the action regardless of the source. It validates the shape of the claim rather than its origin, whether that origin is a human, a large language model, or an energy-based model.[2]
Lineage
The concept draws from several established disciplines in formal methods and software engineering.
Proof-carrying code
Proof-carrying code (PCC), introduced by George C. Necula in 1997, is code that ships with a machine-checkable proof of its safety properties. The consumer verifies the proof without trusting the producer.[3] Proofware generalizes this approach from low-level code safety to application-level invariants.[1]
Design by contract
Design by contract (DbC), formalized by Bertrand Meyer in 1992, treats preconditions, postconditions, and invariants as first-class elements of software.[7] Proofware extends contracts from runtime assertions to compile-time or check-time proofs.[2]
Formal verification
Formal verification is the broader discipline of using mathematical methods to prove that a system satisfies a specification. Proofware applies this specifically at the trust boundary layer rather than attempting to verify the entire system state.[5]
Proof assistants
Proof assistants such as Lean 4, Coq, and Isabelle are interactive theorem provers that allow constraints to be written as code and produce machine-checked proofs.[8] These tools provide the mechanism for writing proofware boundaries.
Energy-based models
Energy-based models for reasoning perform constraint satisfaction via energy minimization, scoring whole states rather than decoding tokens sequentially.[9] In a proofware architecture, the output of such models is treated as untrusted input that must pass the formally verified boundary.[2]
Distinction from related concepts
Proofware functions as the boundary layer of an application rather than a full application.[1] It differs from a testing framework in that tests rely on sampling, whereas proofware relies on proofs.[3] It is not specific to any single runtime.