# CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

## Project Overview

This is a PhD thesis proposal for developing a methodology to build High-Assurance Hybrid Autonomous Control Systems (HAHACS) for critical infrastructure. The proposal is titled "From Cold Start to Critical: Formal Synthesis of Autonomous Hybrid Controllers."

**Intellectual Merit**: The contribution is architectural unification rather than algorithmic novelty. The methodology provides a systematic decomposition mapping verification techniques to control mode types, composing existing formal methods into a complete framework where none existed.

**Key Insight**: The methodology formalizes EXISTING discrete abstractions from operating procedures (especially nuclear) rather than imposing arbitrary ones. Operating procedures already define go/no-go conditions as discrete predicates - this work provides the formalization and verification framework.

## Document Structure

The proposal uses a modular LaTeX structure with numbered section directories:
- `main.tex` - Root document that inputs all sections
- `1-goals-and-outcomes/` - Research statement and goals
- `2-state-of-the-art/` - Literature review
- `3-research-approach/` - Core methodology (CURRENTLY ACTIVE WORK)
- `4-metrics-of-success/` - Success criteria
- `5-risks-and-contingencies/` - Risk analysis
- `6-broader-impacts/` - Broader impacts
- `8-schedule/` - Timeline

Each section directory contains:
- `v1.tex` (or `v2.tex` for actively revised sections) - Main content
- `outline.md` (optional) - Planning notes and structure

**IMPORTANT**: Section 3 (research-approach) is currently being revised. `main.tex` inputs `v2.tex` for this section, which contains extensive inline comments and questions prefixed with `%` and `% Q:`.

## Building the Document

```bash
# Full build with bibliography
pdflatex main.tex
bibtex main
pdflatex main.tex
pdflatex main.tex

# Quick build (no bibliography updates)
pdflatex main.tex

# Use latexmk for automated builds
latexmk -pdf main.tex

# Clean auxiliary files
latexmk -c
```

The output is `main.pdf`.

## Key Technical Concepts

### Mathematical Notation
- **Continuous state space**: X ⊆ ℝⁿ
- **Discrete modes**: Q = {q₁, q₂, ...}
- **Per-mode continuous regions**: X_entry,i, X_exit,i, X_safe,i
- **Discrete predicates**: pᵢ: X → {true, false} (Boolean functions over continuous state)

### Three Control Mode Types
Each mode type has distinct control objectives and verification methods:

1. **Transitory modes**: Transition between discrete states
   - Objective: reach(X_entry) → reach(X_exit) while maintaining x(t) ∈ X_safe
   - Verification: Reachability analysis
   - Formal: Reach(X_entry, f(x,u), T) ⊆ X_exit ∪ X_safe

2. **Stabilizing modes**: Maintain steady state
   - Objective: remain(X_target) where X_target ⊂ X_safe
   - Verification: Barrier certificates
   - Formal: ∇B(x)·f(x,u) ≤ 0 on boundary ∂X_safe

3. **Expulsory modes**: Safe shutdown under failures
   - Objective: reach(X_current) → reach(X_safe_shutdown) under parametric uncertainty
   - Verification: Parametric robust reachability
   - Formal: Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure

### Scope Boundaries
- **Verify** continuous controllers, not **synthesize** them (analogous to model checking)
- Assume controllers can be designed using standard control theory
- Contribution is verification that candidate controllers compose correctly with discrete layer

## Active Development Context

### Current Focus (as of 2026-01-26)
Editing the research approach section (`3-research-approach/v2.tex`) with a Wednesday (2026-01-28) draft deadline.

### Open Technical Questions
Questions are embedded in `v2.tex` comments. Key unresolved issues:

**Easier to address:**
- Hysteresis and sensor noise handling (standard control theory)
- Mealy machine formalization (presentation issue)
- Failure detection scope boundaries (precision in claims)

**More challenging:**
- Timing constraint verification (timed automata integration)
- Parametric uncertainty bounds methodology
- Numerical precision in discrete abstraction (task 36 in taskwarrior)
- Controller design gap (scope vulnerability)

### Taskwarrior Integration
The user tracks tasks in taskwarrior. The Thesis project has ~45 tasks including:
- 9 writing tasks for research approach sections (due 2026-01-28)
- Multiple reading tasks on hybrid systems, reachability, formal methods
- Outstanding question (task 36): "How do we handle numerical barriers when creating discrete automata?"

Use `task list project:Thesis` to see current tasks.

## Bibliography

References are in `references.bib` using IEEE transaction format. The bibliography includes:
- Hybrid systems theory and verification
- Formal methods (reactive synthesis, temporal logic)
- Control theory (reachability, barrier certificates)
- Nuclear regulatory documents (NUREG, 10 CFR)
- Industrial control systems

## Custom LaTeX Class

`dane_proposal_format.cls` provides:
- NSF-compliant formatting (Times New Roman, 1" margins)
- Custom `\task{title}{description}` command for numbered tasks
- TikZ libraries for diagrams
- Table and figure formatting
- Default metadata (title, author, advisor)

## Writing Style Notes

- Inline comments in `.tex` files starting with `%` are working notes
- Comments with `% Q:` indicate open questions requiring research/decisions
- Sections marked with `\iffalse ... \fi` are draft text, not compiled
- Text after `\iffalse` blocks are outlines/notes for future writing