DailySafe · Technology and research
Daily safety briefings and work confirmations affect real people. That is why the provenance of a record, the rules then in force, the sequence of corrections and independent reproducibility all matter.
We combine construction-site experience with mathematical methods to define events precisely and validate outcomes.
6 research areas
6 evidence groups
76 targeted tests passed
CI results of 4 November 2026
An interview analysis report by Vadim Akulenko, PhD, examines ten accounts of timekeeping in construction, manufacturing and other work settings. These findings are exploratory rather than population-representative.
View research findings →Six areas connect practical safety workflows with formal models and tested software mechanisms.
TBM attendance, hours, disputes and corrections are represented as related but distinct events. The history of how a result was obtained matters as much as the value displayed.
Backend mechanisms and tests cover record provenance and correction history.
Applying a new policy retroactively to an earlier acknowledgement changes what that record means. The research binds a decision to policy content, version and effective time.
Lean 4 policy-pinning theorems and separate backend tests of policy snapshots and rejection of retroactive TBM are documented.
Core rules are represented as a mathematical model. Machine-checked proofs address policy pinning, evidence provenance, abstract append preservation and model pipeline consistency.
The formal claims apply to the mathematical model, not automatically to the entire app, database or deployed service.
Signed checkpoints and replay verification are used to detect specified tampering, deletion and rollback scenarios.
On 4 November 2026, 76 targeted M4/M5 software tests passed, including a separate witness process and offline verification. This does not establish independently hosted production protection.
Management rights in one organization must not silently apply to another. A worker's confirmation of one hours value must not be reused for a changed value.
The technical evidence register documents negative and positive API-path and database-semantic tests.
The research connects recorded hours, management decisions, worker disputes and corrections. Certain filings address evidence-bounded settlement and localized dispute handling.
A filed research idea is neither a granted patent nor proof that every described function is available in the app.
Each claim is connected to its source and explicitly scoped to what the evidence actually establishes.
Documents invariants, API/DB tests and boundaries for history, access control and value confirmations.
Evidence boundary: A technical record, not a certificate of production deployment.
Evidence · E-01 →Lean 4 theorems A2_policy_pinning_strict and A3_deny_retroactive_strict are mapped to product policy semantics.
Evidence boundary: A model-level proof is not whole-product formal verification.
Evidence · E-02 →Documents A5_append_only, A0_event_provenance_strict, pipeline_consistent and related theorems.
Evidence boundary: The correspondence to FastAPI/PostgreSQL implementation requires separate verification.
Evidence · E-03 →76/76 targeted CI tests passed, covering tampering, deletion, rollback, a separate HTTP process, public-key verification and retroactive-TBM rejection.
Evidence boundary: Software CI evidence, not independently governed production-host evidence.
Evidence · E-04 →Documents tests for cross-organization denials, authority-at-effect and changed values after confirmation.
Evidence boundary: Covers specified API/DB paths, not every possible threat.
Evidence · E-05 →Reconciles selected DailySafe-related filings with the private filing register.
Evidence boundary: Filing is not patent grant or proof of implemented coverage.
Evidence · E-06 →A separate catalogue lists the application numbers and themes for event evidence, policy versions, work settlement and verification. A filed application is neither a granted patent nor proof of complete product implementation.
View application catalogue →A mathematical proof of a model, a passing software test and a guarantee enabled on a live job site are three different levels of evidence. We keep them distinct.