CodexPM

Overview

A formal specification language for computer systems that enables unambiguous system definitions, automated verification, and standards compliance checking — separating the formalization from the implementation.

Problem

System specifications today are written in natural language (docs, wikis, tickets) and are ambiguous by nature. There’s no way to automatically verify that an implementation matches its specification, or that the specification itself complies with a given standard.

Approach

• Define an unambiguous formal language for specifying system behavior
• Separate the formalization/specification from the implementation
• A formalization can be verified and audited against standards automatically
• Code is written to match the formalization — if it matches, it automatically complies with the standard
• Support trade-off analysis between different design choices

Flow Specification

Explicitly describe how users access the software:

• User environment (internet / intranet)
• Browser
• Domain resolution / DNS
• Reverse proxy
• SWA (static web app)
• API
• Identity provider (IdP)

Example

Formalize authentication processes with all systems involved. The formal specification defines required structures (client, IdP, protected resource, etc.). The code is then written to match — if it matches, the software automatically complies with the authentication standard.

Open Questions

• What existing formal methods (TLA+, Alloy, Z notation) can be built upon?
• How to make the language accessible to non-academics?
• How to bridge the gap between formal spec and actual code verification?
• What standards to target first for compliance checking?

References

Log