proof-carrying-code-generator

Proof-Carrying Code Generator

Generate executable code bundled with formal proofs that certify key safety and correctness properties.

Overview

Proof-carrying code (PCC) is executable code accompanied by formal proofs that certify specific properties. This skill helps generate:

1. Verified implementations with correctness proofs
2. Safety certificates for memory safety, bounds checking, null safety
3. Functional specifications with pre/postconditions
4. Invariant proofs for data structure integrity
5. Extracted code from verified specifications

The generated code can be extracted to mainstream languages (OCaml, Haskell, SML) while maintaining proof certificates.

PCC Generation Workflow

Requirements
    ↓
Formal Specification
    ↓
Verified Implementation
    ↓
Proof Obligations
    ↓
Certified Code + Proofs
    ↓
Code Extraction

Core Approaches

Approach 1: Specification-First

Start with formal specification, implement, then prove.

Steps:

1. Write formal specification
2. Implement function/algorithm
3. State correctness theorem
4. Prove theorem
5. Extract code

Example (Isabelle):

(* Specification *)
definition sorted_spec :: "nat list ⇒ nat list ⇒ bool" where
  "sorted_spec input output ≡ sorted output ∧ mset output = mset input"

(* Implementation *)
fun insertion_sort :: "nat list ⇒ nat list" where
  "insertion_sort [] = []" |
  "insertion_sort (x # xs) = insert x (insertion_sort xs)"

(* Correctness theorem *)
theorem insertion_sort_correct:
  "sorted_spec input (insertion_sort input)"
proof (induction input)
  case Nil
  then show ?case by (simp add: sorted_spec_def)
next
  case (Cons x xs)
  then show ?case
    using insert_sorted mset_insert
    by (auto simp: sorted_spec_def)
qed

(* Extract code *)
export_code insertion_sort in SML file "sort.sml"

Approach 2: Refinement-Based

Start abstract, refine to concrete with proofs at each step.

Steps:

1. Abstract specification
2. Refine to intermediate level
3. Prove refinement correct
4. Refine to executable code
5. Prove final refinement
6. Extract code