Wikipedia

Draft:Proofware



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]
edit
ConceptRelationship to proofware
Proof assistantA tool for constructing and checking formal proofs. Proofware is the proof-bearing software artifact or architecture, not the tool alone.[3]
Proof-carrying codeA 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 verificationThe broader discipline of proving that systems satisfy specifications. Proofware refers to software artifacts or architectures that incorporate such proofs.[5]
TestingTesting samples executions; proofware relies on formal proof for stated properties, although tested components may still exist in the surrounding system.[4]

See also

edit

References

edit
  1. 1 2 3 4 5 6 7 8 Pientka, Brigitte (2013). "Proofware: establishing trustworthy computing through programming with proofs". Natural Sciences and Engineering Research Council. Retrieved 2026-02-06.
  2. 1 2 Blanco, Rob (2013). Proofware: verified computation and proof-carrying architectures (Ph.D. Thesis). McGill University.
  3. 1 2 3 4 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.
  4. 1 2 3 4 5 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.
  5. 1 2 3 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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Draft:Proofware&oldid=1362680526"