sc30gsw/vcsdd-formal-hardening

VCSDD Formal Hardening

When to Activate

• Phase 5 (formal hardening)
• Writing verification harnesses
• Interpreting property test failures

Tool Selection by Tier

| Tier | Rust | Python | TypeScript | |------|------|--------|------------| | 1 | proptest, cargo-fuzz | hypothesis | fast-check | | 2 | kani | (manual invariants) | (manual invariants) | | 3 | kani + CBMC | (escalate to human) | (escalate to human) |

Proof Harness Patterns

Rust - Kani (Tier 2)

#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    fn verify_parse_empty() {
        let result = parse("");
        assert!(result == Err(ParseError::Empty));
    }

    #[kani::proof]
    #[kani::unwind(10)]
    fn verify_parse_roundtrip() {
        let input: String = kani::any();
        kani::assume(input.len() < 10);
        if let Ok(parsed) = parse(&input) {
            assert_eq!(serialize(parsed), input);
        }
    }
}

Python - Hypothesis (Tier 1)

from hypothesis import given, strategies as st

@given(st.text(min_size=0, max_size=100))
def test_parse_arbitrary(s):
    result = parse(s)
    if result.is_ok():
        assert serialize(result.value) == s

TypeScript - fast-check (Tier 1)

import * as fc from 'fast-check';

test('parse roundtrip', () => {
  fc.assert(
    fc.property(fc.string({ minLength: 0, maxLength: 100 }), (s) => {
      const result = parse(s);
      if (result.ok) {
        return serialize(result.value) === s;
      }
      return true; // error cases are valid
    })
  );
});

Graceful Degradation

Always produce:

1. verification-report.md
2. security-report.md
3. purity-audit.md
4. At least one captured file under verification/security-results/

If required tool is unavailable:

1. Document the degradation in verification-report.md
2. Degrade to lower tier
3. Only leave an obligation as skipped when it is not required
4. Still run security hardening / purity audit and write their artifacts
5. Required obligations that remain skipped block Phase 6
6. Pipeline DOES NOT block if obligation is not required