Work
Selected work.
Client names appear only under signed agreements. The work is described plainly and generically; the decisions are real.
01 · Clinical systems · In deployment
Paper to practice, one machine.
A single-chair dental practice, previously paper-only, moving onto an open-source practice-management system with 0pon as the integrator. The design decision that shapes everything else: the entire system lives on one machine in the clinic. No hosted VM, no VPN, no cloud dependency, no monthly infrastructure bill worth naming. Patient records never leave the room they are used in.
The discipline is in the unglamorous parts. Backups exist only when a restore has actually been performed, so restores are rehearsed before go-live, not after the first loss. Retention and access follow the practice's local data-protection law, written down, not assumed. The practice owns its own licenses and its own data; 0pon holds neither.
02 · Verified systems · Research
n0de: access control that carries a proof.
n0de is an access engine for multi-level data: one identity holding many compartments at once, with the confidentiality properties machine-checked in Lean 4. No read-up and no write-down across level, compartment, and need-to-know. Non-interference: activity in a compartment provably cannot change what an outsider sees. Existence itself does not leak. Revoking a compartment cuts cleanly, with on-disk residue provably unable to influence what a de-accessed user can observe.
The proofs are not decoration. The policy engine (Cedar) is differentially checked against the proven model, and the PostgreSQL row-level-security predicate that enforces decisions is proven faithful to it in both directions, so the deployed SQL cannot silently drift from the theorem. Built entirely on open parts. An SBIR proposal building on this work is under review.