Draft:Proofware
 | Review waiting, please be patient.
This may take 5 weeks or more, since drafts are reviewed in no specific order. There are 2,187 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
|
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]
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
[edit]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
[edit]The concept draws from several established disciplines in formal methods and software engineering.
Proof-carrying code
[edit]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
[edit]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
[edit]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
[edit]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
[edit]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
[edit]| Term | Description |
|---|---|
| Vaporware | Software announced and delayed into irrelevance; never ships or ships too late.[10] |
| Proofware | Software shipping formally verified boundaries; constraints are enforced by a proof.[1] |
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.
See also
[edit]- Formal methods
- Formal verification
- Proof-carrying code
- Design by contract
- Vaporware
- Lean (proof assistant)
References
[edit]- ^ a b c d e f Pientka, Brigitte (2013). "Proofware: establishing trustworthy computing through programming with proofs". Natural Sciences and Engineering Research Council. Retrieved 2026-02-06.
- ^ a b c d Blanco, Rob (2013). Proofware: verified computation and proof-carrying architectures (Ph.D. Thesis). McGill University.
- ^ a b c Necula, George C. (1997). Proof-Carrying Code. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM. pp. 106–119. doi:10.1145/263699.263712.
- ^ Schneider, Fred B. (1990). "Implementing Fault-Tolerant Services Using the State Machine Approach". ACM Computing Surveys. 22 (4): 299–319. doi:10.1145/98163.98167.
- ^ a b Clarke, Edmund M.; Emerson, E. Allen; Sifakis, Joseph (2009). "Model Checking: Algorithmic Verification and Debugging". Communications of the ACM. 52 (11): 74–84. doi:10.1145/1592761.1592781.
- ^ Anderson, James P. (1972). Computer Security Technology Planning Study (Technical report). United States Air Force. ESD-TR-73-51.
- ^ Meyer, Bertrand (1992). "Applying 'Design by Contract'". IEEE Computer. 25 (10): 40–51. doi:10.1109/2.161279.
- ^ de Moura, Leonardo; Ullrich, Sebastian (2021). The Lean 4 Theorem Prover and Programming Language. 28th International Conference on Automated Deduction (CADE-28). Springer. doi:10.1007/978-3-030-79876-5_37.
- ^ LeCun, Yann; Chopra, Sumit; Hadsell, Raia; Ranzato, M.; Huang, F. (2006). "A Tutorial on Energy-Based Learning". Predicting Structured Data. MIT Press.
- ^ Barry, M. (2001). "Vaporware: The Software That Never Was". PC World.