# Formal Methods

> Formal verification methods

- Skill: `ffsshhttiikk/formal-methods` (Agent Skill)
- Install (CLI): `npx skillmds@latest add ffsshhttiikk/formal-methods`
- Raw SKILL.md: https://api.skillmd.com/api/skills/ffsshhttiikk/formal-methods/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- License: MIT
- Author: ffsshhttiikk (https://skillmd.com/u/ffsshhttiikk)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/ffsshhttiikk/formal-methods

---


## What I do
- Specify system behavior formally
- Verify correctness of algorithms
- Prove properties about programs
- Model check systems

## When to use me
When building high-assurance systems where correctness is critical.

## Formal Specification

### Pre/Post Conditions
```python
class FormalSpec:
    """Design by contract"""
    
    def requires(self, *conditions):
        """Precondition decorator"""
        def decorator(func):
            def wrapper(*args, **kwargs):
                for i, cond in enumerate(conditions):
                    if not cond(args[i] if i < len(args) else None):
                        raise PreconditionViolation(
                            f"Precondition {cond.__name__} failed"
                        )
                return func(*args, **kwargs)
            return wrapper
        return decorator
    
    def ensures(self, *conditions):
        """Postcondition decorator"""
        def decorator(func):
            def wrapper(*args, **kwargs):
                result = func(*args, **kwargs)
                for cond in conditions:
                    if not cond(result):
                        raise PostconditionViolation(
                            f"Postcondition {cond.__name__} failed"
                        )
                return result
            return wrapper
        return decorator


# Example: Sorted list specification
def is_sorted(lst: list) -> bool:
    """Postcondition: list is sorted"""
    for i in range(len(lst) - 1):
        if lst[i] > lst[i + 1]:
            return False
    return True


def non_negative(x: int) -> bool:
    """Precondition: x is non-negative"""
    return x >= 0


def sorted_insert(lst: list, x: int) -> list:
    """Insert x into sorted list lst"""
    result = lst + [x]
    result.sort()
    return result
```

### Invariants
```python
class Invariant:
    """Class and loop invariants"""
    
    @staticmethod
    def class_invariant(cls):
        """Decorator for class invariant"""
        original_init = cls.__init__
        
        def new_init(self, *args, **kwargs):
            original_init(self, *args, **kwargs)
            if not cls.invariant(self):
                raise InvariantViolation("Class invariant violated")
        
        cls.__init__ = new_init
        
        # Check invariant after each public method
        original_methods = [m for m in dir(cls) 
                          if not m.startswith('_') 
                          and callable(getattr(cls, m))]
        
        for method_name in original_methods:
            original_method = getattr(cls, method_name)
            
            def make_wrapper(method):
                def wrapper(self, *args, **kwargs):
                    result = method(self, *args, **kwargs)
                    if not cls.invariant(self):
                        raise InvariantViolation(
                            f"Invariant violated after {method_name}"
                        )
                    return result
                return wrapper
            
            setattr(cls, method_name, make_wrapper(original_method))
        
        return cls


# Example: Stack invariant
@Invariant
class Stack:
    def __init__(self, capacity: int):
        self.items = []
        self.capacity = capacity
    
    def invariant(self):
        """Stack invariant"""
        return (
            len(self.items) >= 0 and
            len(self.items) <= self.capacity
        )
    
    def push(self, item):
        if len(self.items) >= self.capacity:
            raise OverflowError("Stack overflow")
        self.items.append(item)
    
    def pop(self):
        if not self.items:
            raise IndexError("Stack underflow")
        return self.items.pop()
```

### Formal Verification

### Hoare Logic
```python
class HoareTriple:
    """Hoare logic for program verification"""
    
    @staticmethod
    def verify(Pre: Callable, program: Callable, 
              Post: Callable) -> bool:
        """Verify Hoare triple: {P} program {Q}"""
        # In practice, use theorem prover
        pass
    
    @staticmethod
    def assignment(x: str, expr: str, post: str) -> str:
        """Hoare rule for assignment: {Q[x/E]} x := E {Q}"""
        return f"{{{post.replace(x, expr)}}}"
    
    @staticmethod
    def sequence(stmts: List[str], pre: str, post: str) -> str:
        """Hoare rule for sequence"""
        # {P} S1; S2 {R} from {P} S1 {Q}; {Q} S2 {R}
        return pre
    
    @staticmethod
    def conditional(pre: str, cond: str, 
                   post_then: str, post_else: str) -> str:
        """Hoare rule for if"""
        # {P} if B then {Q} else {R} from {P && B} S1 {Q} and {P && !B} S2 {R}
        return f"{{{pre}}}"
```

### Model Checking
```python
class ModelChecker:
    """Simple model checker"""
    
    def __init__(self):
        self.states = set()
        self.transitions = {}
        self.properties = []
    
    def add_state(self, state: str):
        self.states.add(state)
    
    def add_transition(self, from_state: str, to_state: str, 
                      action: str):
        if from_state not in self.transitions:
            self.transitions[from_state] = []
        self.transitions[from_state].append((action, to_state))
    
    def check_reachability(self, start: str, goal: str) -> bool:
        """Check if goal is reachable from start"""
        visited = set()
        stack = [start]
        
        while stack:
            state = stack.pop()
            if state == goal:
                return True
            if state in visited:
                continue
            
            visited.add(state)
            
            for _, next_state in self.transitions.get(state, []):
                stack.append(next_state)
        
        return False
    
    def check_liveness(self, start: str, good_states: Set[str]) -> bool:
        """Check liveness: eventually reach good state"""
        visited = set()
        stack = [start]
        
        while stack:
            state = stack.pop()
            if state in visited:
                continue
            
            visited.add(state)
            
            if state in good_states:
                return True
            
            for _, next_state in self.transitions.get(state, []):
                stack.append(next_state)
        
        return False
    
    def check_safety(self, start: str, 
                    bad_states: Set[str]) -> bool:
        """Check safety: never reach bad state"""
        return not self.check_reachability(start, 
            bad_states.pop() if bad_states else None)
```