ENGINEERING · RESEARCH
Formal verification methods
Investigation of how formal methods could apply to ranking, audit safety, and control-plane logic — without claiming deployed proofs today.
RESEARCHExecutive
Formal verification aims to prove properties of systems with mathematical rigor. FoxHeight’s current platform uses deterministic algorithms, explicit maturity labels, and automated tests. This page records an engineering investigation into where formal methods may later add value — and where they are not yet justified.
Technical
Candidate properties for formal treatment in Continuum-like systems:
- SSRF safety: no private-network reachability from the public auditor (partially enforced by runtime checks today).
- Ranking monotonicity: increasing a positively weighted feature does not decrease score under fixed weights.
- Session integrity: unauthenticated actors cannot access portal routes.
- Upload path confinement: stored files remain under the media root.
Architecture
A pragmatic split:
Lightweight model checking and property-based tests are nearer-term than full theorem proving for a PHP/Node local-first stack.
Research
- Question: Which Continuum invariants are both security-critical and tractable to formalize?
- Hypothesis: Network-egress policies and ranking algebra are more tractable than full application semantics.
- Methodology: Property listing, adversary models, comparison of runtime checks vs formal specs.
- Limitations: No machine-checked proofs are shipped in this repository. Tests and runtime guards are the current evidence base.
Methods under investigation
| Method | Fit | Status at FoxHeight |
|---|---|---|
| Runtime assertion / contracts | High | Partial (validation helpers) |
| Property-based testing | High | Research candidate |
| Model checking (protocol-scale) | Medium | Not implemented |
| Deductive theorem proving | Low near-term | Not implemented |
| Static type discipline | Medium | PHP strict types; limited TS surface |
Evidence
Current verification evidence is empirical: PHP syntax suite, ranking/search/audit unit tests, SSRF deny tests. Formal proofs are not claimed.
Future
Any future formal verification work will be labelled RESEARCH or PROTOTYPE until proofs or checked models exist in-repo.