The underlying GitHub engineering repositories are private. This page gives disclosure-safe results, record dates and stated limits. It does not replace original test logs or independent certification.
Formal model proofs, passing software tests and verified production deployments are distinct levels of evidence.
What was checked: Documents invariants, API/DB tests and boundaries for history, access control and value confirmations.
Limitations: A technical record, not a certificate of production deployment.
What was checked: Lean 4 theorems A2_policy_pinning_strict and A3_deny_retroactive_strict are mapped to product policy semantics.
Limitations: A model-level proof is not whole-product formal verification.
What was checked: Documents A5_append_only, A0_event_provenance_strict, pipeline_consistent and related theorems.
Limitations: The correspondence to FastAPI/PostgreSQL implementation requires separate verification.
What was checked: 76/76 targeted CI tests passed, covering tampering, deletion, rollback, a separate HTTP process, public-key verification and retroactive-TBM rejection.
Limitations: Software CI evidence, not independently governed production-host evidence.
What was checked: Documents tests for cross-organization denials, authority-at-effect and changed values after confirmation.
Limitations: Covers specified API/DB paths, not every possible threat.
What was checked: Reconciles selected DailySafe-related filings with the private filing register.
Limitations: Filing is not patent grant or proof of implemented coverage.
Primary records are retained privately and may be reviewed separately by authorized parties under agreed access conditions.