Draft:Proofware
 | Review waiting, please be patient.
This may take 4 months or more, since drafts are reviewed in no specific order. There are 4,518 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
|
Submission declined on 27 April 2026 by BlueStaticHorse (talk). This draft appears to be a duplicate of an existing article. Wikipedia does not permit multiple articles on the same topic.
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
This draft has been resubmitted and is currently awaiting re-review. |  |
Proofware is a term used in formal methods research for software artifacts and programming practices in which machine-checkable proofs are developed as part of the software system.[1] The term has been used in work on trustworthy computing through programming with proofs and in research on verified computation and proof-carrying architectures.[2]
Proofware is closely related to proof assistants, proof-carrying code, certified programming, and formal verification, but it refers to the proof-bearing software artifact or architecture rather than only to the tool used to construct the proof. A proof assistant may be used to create proofware, while proofware is the resulting software, proof, or verified boundary that can be checked by a machine.[1]
Relationship to proof assistants
[edit]Proof assistants such as Lean, Coq, and Isabelle are interactive theorem provers used to write and check formal proofs.[3] Proofware is not itself a proof assistant. It is the software or software-design artifact produced when machine-checkable proofs are integrated into the system being built.[1]
This distinction is similar to the distinction between a compiler and compiled software: a proof assistant is a tool, while proofware is an artifact or system whose correctness claims depend on proofs produced or checked by such tools.
Background
[edit]The idea of software accompanied by machine-checkable evidence is associated with several established areas of formal methods.
Proof-carrying code
[edit]Proof-carrying code (PCC), introduced by George C. Necula in 1997, is a mechanism in which code is distributed with a machine-checkable proof of safety properties. The host verifies the proof before accepting or executing the code.[4] Proofware research generalizes this proof-bearing approach beyond low-level code safety into broader programming-with-proofs settings.[1]
Certified programming
[edit]Certified programming uses formal specifications and machine-checked proofs to establish properties of programs. In this setting, the program and the proof are developed together, often with a proof assistant or related verification tool.[3] Proofware may be understood as a software artifact in which this proof-bearing structure is part of the delivered system or architecture.[1]
Formal verification
[edit]Formal verification is the use of mathematical methods to prove that a system satisfies a formal specification.[5] Proofware is one way formal verification can appear as part of software construction: proofs are not only external documentation, but artifacts connected to the program or system being checked.[1]
Characteristics
[edit]Descriptions of proofware emphasize the use of machine-checkable proofs in the construction of trustworthy software systems.[1] Common characteristics include:
- Machine-checkable proof: correctness or safety claims are represented as formal proofs that can be checked by software rather than accepted only by informal review.[4]
- Connection to software artifacts: the proof is associated with code, a verified component, or a software architecture rather than existing only as a mathematical result.[2]
- Reduced trust in producers: as in proof-carrying code, the consumer or checker verifies the proof instead of relying only on the authority of the code producer.[4]
- Use of formal-methods tools: proof assistants, model checkers, and related verification systems may be used to construct or check the proofs.[5][3]
Distinction from related concepts
[edit]| Concept | Relationship to proofware |
|---|---|
| Proof assistant | A tool for constructing and checking formal proofs. Proofware is the proof-bearing software artifact or architecture, not the tool alone.[3] |
| Proof-carrying code | A specific mechanism in which code is distributed with a proof of safety. Proofware is a broader term used for programming with proofs and verified computation artifacts.[4][1] |
| Formal verification | The broader discipline of proving that systems satisfy specifications. Proofware refers to software artifacts or architectures that incorporate such proofs.[5] |
| Testing | Testing samples executions; proofware relies on formal proof for stated properties, although tested components may still exist in the surrounding system.[4] |
See also
[edit]- Certified programming
- Design by contract
- Formal methods
- Formal verification
- Proof assistant
- Proof-carrying code
- Theorem prover
References
[edit]- ^ a b c d e f g h Pientka, Brigitte (2013). "Proofware: establishing trustworthy computing through programming with proofs". Natural Sciences and Engineering Research Council. Retrieved 2026-02-06.
- ^ a b Blanco, Rob (2013). Proofware: verified computation and proof-carrying architectures (Ph.D. Thesis). McGill University.
- ^ a b c d 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.
- ^ a b c d e 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.
- ^ a b c 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.