hyperpolymath · hyperpolymath · Jun 20, 2026 · Jun 20, 2026 · Jun 20, 2026 · Jun 20, 2026
@@ -37,6 +37,25 @@ jobs:
         uses: github/codeql-action/upload-sarif@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v4
         with:
           sarif_file: results.sarif
+      - name: Upload results artifact
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: scorecard-sarif
+          path: results.sarif
+          retention-days: 1
+  # The score gate runs in a separate job so the publish job (which holds the
+  # OIDC id-token) contains no custom run steps.
+  score-gate:
+    needs: scorecard
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - name: Download results artifact
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093 # v4.3.0
+        with:
+          name: scorecard-sarif
       - name: Check minimum score
         run: |
           # Parse score from results

@@ -16,11 +16,12 @@ jobs:
     secrets: inherit
   trufflehog:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332
         with:
           fetch-depth: 0
       - name: TruffleHog Secret Scan
-        uses: trufflesecurity/trufflehog@main
+        uses: trufflesecurity/trufflehog@30d5bb91af1a771378349dbbb0c82129392acf70 # v3.95.6
         with:
           extra_args: --only-verified --fail
@@ -1,24 +1,22 @@
-<!--
-SPDX-License-Identifier: MPL-2.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# Phronesis Academic Documentation
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+== Phronesis Academic Documentation
 
-**SPDX-License-Identifier: MPL-2.0
 
 This directory contains comprehensive academic documentation for Phronesis, including formal proofs, white papers, and mechanized verification. The documentation is designed to withstand rigorous academic scrutiny across multiple fields of mathematics and computer science.
 
----
+'''''
 
-## Overview
+=== Overview
 
 Phronesis is a formally verified consensus-gated policy language for network configuration. This documentation provides rigorous mathematical foundations suitable for academic peer review, covering 20+ areas of mathematics and computer science.
 
----
+'''''
 
-## Directory Structure
+=== Directory Structure
 
-```
+....
 academic/
 ├── papers/
 │   └── phronesis-white-paper.md              # Main academic paper
@@ -113,84 +111,100 @@ academic/
 ├── notation-guide.md                         # Unified notation reference
 ├── theorem-index.md                          # Cross-referenced theorem index
 └── TODO.md                                   # Remaining work items
-```
-
----
-
-## Complete Theorem Coverage
-
-### Foundations (120+ Theorems)
-
-| Area | Key Theorems | Document |
-|------|--------------|----------|
-| **Type Theory** | Progress, Preservation, Strong Normalization | type-theory-proofs.md |
-| **Category Theory** | Functor Laws, Monad Laws, CCC Structure | category-theory-foundations.md |
-| **Domain Theory** | CPO Completeness, Scott Continuity, Fixed Points | domain-theory-foundations.md |
-| **Order Theory** | Well-Foundedness, WQO Closure, Lattice Properties | order-theory-foundations.md |
-| **Set Theory** | ZFC Axioms, Cardinality, Transfinite Induction | set-theoretic-foundations.md |
-
-### Semantics
-
-| Area | Key Theorems | Document |
-|------|--------------|----------|
-| **Operational** | Determinism, Totality, 45+ Rules | complete-operational-semantics.md |
-| **Denotational** | Compositionality, Adequacy, Full Abstraction | denotational-semantics.md |
-| **Axiomatic** | Soundness, Completeness, WP Characterization | hoare-logic.md |
-| **Algebraic** | Initial Algebra, Catamorphism, Hylomorphism | algebraic-semantics.md |
-
-### Security
-
-| Area | Key Theorems | Document |
-|------|--------------|----------|
-| **Information Flow** | Noninterference, TINI, Declassification | information-flow-analysis.md |
-| **Cryptography** | EUF-CMA, BFT Safety, UC Security | cryptographic-proofs.md |
-| **Protocol** | Authentication, Agreement, Replay Prevention | dolev-yao-model.md |
-| **Separation Logic** | Frame Rule, Capability Isolation | separation-logic.md |
-
-### Consensus
-
-| Area | Key Theorems | Document |
-|------|--------------|----------|
-| **Game Theory** | Nash Equilibrium, Incentive Compatibility | consensus-game-theory.md |
-| **Temporal Logic** | Safety, Liveness, Fairness | temporal-logic-specifications.md |
-| **Concurrency** | Deadlock Freedom, Bisimulation | process-algebra.md |
-| **Probability** | Vote Distribution, Tail Bounds | probabilistic-analysis.md |
+....
+
+'''''
+
+=== Complete Theorem Coverage
+
+==== Foundations (120+ Theorems)
+
+[cols=",,",options="header",]
+|===
+|Area |Key Theorems |Document
+|*Type Theory* |Progress, Preservation, Strong Normalization |type-theory-proofs.md
+|*Category Theory* |Functor Laws, Monad Laws, CCC Structure |category-theory-foundations.md
+|*Domain Theory* |CPO Completeness, Scott Continuity, Fixed Points |domain-theory-foundations.md
+|*Order Theory* |Well-Foundedness, WQO Closure, Lattice Properties |order-theory-foundations.md
+|*Set Theory* |ZFC Axioms, Cardinality, Transfinite Induction |set-theoretic-foundations.md
+|===
+
+==== Semantics
+
+[cols=",,",options="header",]
+|===
+|Area |Key Theorems |Document
+|*Operational* |Determinism, Totality, 45+ Rules |complete-operational-semantics.md
+|*Denotational* |Compositionality, Adequacy, Full Abstraction |denotational-semantics.md
+|*Axiomatic* |Soundness, Completeness, WP Characterization |hoare-logic.md
+|*Algebraic* |Initial Algebra, Catamorphism, Hylomorphism |algebraic-semantics.md
+|===
+
+==== Security
+
+[cols=",,",options="header",]
+|===
+|Area |Key Theorems |Document
+|*Information Flow* |Noninterference, TINI, Declassification |information-flow-analysis.md
+|*Cryptography* |EUF-CMA, BFT Safety, UC Security |cryptographic-proofs.md
+|*Protocol* |Authentication, Agreement, Replay Prevention |dolev-yao-model.md
+|*Separation Logic* |Frame Rule, Capability Isolation |separation-logic.md
+|===
+
+==== Consensus
+
+[cols=",,",options="header",]
+|===
+|Area |Key Theorems |Document
+|*Game Theory* |Nash Equilibrium, Incentive Compatibility |consensus-game-theory.md
+|*Temporal Logic* |Safety, Liveness, Fairness |temporal-logic-specifications.md
+|*Concurrency* |Deadlock Freedom, Bisimulation |process-algebra.md
+|*Probability* |Vote Distribution, Tail Bounds |probabilistic-analysis.md
+|===
+
+==== Language Theory
+
+[cols=",,",options="header",]
+|===
+|Area |Key Theorems |Document
+|*Automata* |DFA Recognition, LL(1) Parsing |automata-theory-proofs.md
+|*Complexity* |O(n) Parsing, P Membership |computational-complexity-analysis.md
+|*Graph Theory* |Valley-Free Routing, Cycle Detection |bgp-graph-theory.md
+|===
+
+'''''
+
+=== Formal Verification Status
+
+[cols=",,,,,",options="header",]
+|===
+|Property |Coq |Lean 4 |Agda |TLA+ |ProVerif
+|Type Safety |✓ |✓ |✓ |- |-
+|Preservation |✓ |✓ |✓ |- |-
+|Determinism |✓ |✓ |✓ |- |-
+|Termination |✓ |✓ |✓ |- |-
+|Subtyping |✓ |✓ |- |- |-
+|Consensus Safety |- |- |- |✓ |-
+|Liveness |- |- |- |✓ |-
+|Authentication |- |- |- |- |✓
+|Noninterference |- |- |- |- |-
+|===
+
+*Legend:*
+
+* ✓ = Fully mechanized and verified
+* `-` = Not applicable or symbolic proof only
+
+'''''
+
+=== Quick Start
+
+==== View Documentation
 
-### Language Theory
-
-| Area | Key Theorems | Document |
-|------|--------------|----------|
-| **Automata** | DFA Recognition, LL(1) Parsing | automata-theory-proofs.md |
-| **Complexity** | O(n) Parsing, P Membership | computational-complexity-analysis.md |
-| **Graph Theory** | Valley-Free Routing, Cycle Detection | bgp-graph-theory.md |
-
----
-
-## Formal Verification Status
-
-| Property | Coq | Lean 4 | Agda | TLA+ | ProVerif |
-|----------|-----|--------|------|------|----------|
-| Type Safety | ✓ | ✓ | ✓ | - | - |
-| Preservation | ✓ | ✓ | ✓ | - | - |
-| Determinism | ✓ | ✓ | ✓ | - | - |
-| Termination | ✓ | ✓ | ✓ | - | - |
-| Subtyping | ✓ | ✓ | - | - | - |
-| Consensus Safety | - | - | - | ✓ | - |
-| Liveness | - | - | - | ✓ | - |
-| Authentication | - | - | - | - | ✓ |
-| Noninterference | - | - | - | - | - |
-
-**Legend:**
-- ✓ = Fully mechanized and verified
-- `-` = Not applicable or symbolic proof only
-
----
-
-## Quick Start
-
-### View Documentation
 All proofs are in Markdown format for easy reading:
-```bash
+
+[source,bash]
+----
 # Main paper
 less academic/papers/phronesis-white-paper.md
 
@@ -199,55 +213,61 @@ less academic/proofs/type-theory/type-theory-proofs.md
 
 # Theorem index
 less academic/theorem-index.md
-```
+----
 
-### Verify Coq Proofs
-```bash
+==== Verify Coq Proofs
+
+[source,bash]
+----
 opam install coq coq-mathcomp
 coqc academic/formal-verification/coq/Phronesis.v
-```
+----
+
+==== Check TLA+ Specification
 
-### Check TLA+ Specification
-```bash
+[source,bash]
+----
 tlc formal/PhronesisConsensus.tla
-```
+----
 
----
+'''''
 
-## Navigation Aids
+=== Navigation Aids
 
-- **notation-guide.md**: Comprehensive notation reference across all documents
-- **theorem-index.md**: Cross-referenced index of 120+ theorems with dependencies
+* *notation-guide.md*: Comprehensive notation reference across all documents
+* *theorem-index.md*: Cross-referenced index of 120+ theorems with dependencies
 
----
+'''''
 
-## Citation
+=== Citation
 
-```bibtex
+[source,bibtex]
+----
 @techreport{phronesis2025,
   title={Phronesis: A Formally Verified Consensus-Gated Policy Language},
   author={Phronesis Development Team},
   year={2025},
   institution={Open Source},
   note={Available at https://github.com/hyperpolymath/phronesis}
 }
-```
+----
 
----
+'''''
 
-## Contributing
+=== Contributing
 
 Academic contributions are welcome. Please:
 
-1. Follow notation conventions in `notation-guide.md`
-2. Include complete proofs with all steps justified
-3. Add theorem to `theorem-index.md` with dependencies
-4. Provide mechanized proofs where possible
-5. Reference existing work appropriately
+[arabic]
+. Follow notation conventions in `notation-guide.md`
+. Include complete proofs with all steps justified
+. Add theorem to `theorem-index.md` with dependencies
+. Provide mechanized proofs where possible
+. Reference existing work appropriately
 
----
+'''''
 
-## License
+=== License
 
 All academic documentation is dual-licensed under Apache-2.0 and MIT.
 See SPDX headers in individual files.