JavaScript (ES6) - 198, 183, 180, 188, 187 bytes

f=s=>/^(:[\da-f]{1,4}){8}$/i.test(':'+(s=s[r='replace'](d='::',':0'.repeat((n=8-s.split(/:+/).length%9)||1)+':')[r](/^:0|0:$/g,n?'0:0':0)))&&[s,s[r](/(\b0(:0)*)(?!.*\1:0)/,d)[r](/::+/,d)]

And, a bit longer, interactive version with some pop-ups (203 bytes):

/^(:[\da-f]{1,4}){8}$/i.test(':'+(s=(s=prompt())[r='replace'](d='::',':0'.repeat((n=8-s.split(/:+/).length%9)||1)+':')[r](/^:0|0:$/g,n?'0:0':0)))&&alert(s+'\n'+s[r](/(\b0(:0)*)(?!.*\1:0)/,d)[r](/::+/,d))

Ungolfed:

function ipv6(str) {
    "use strict";
    var zeros = 8 - str.split(/:+/).length % 9

        ,longIP = str
            .replace('::', ':0'.repeat(zeros || 1) + ':')
            .replace(/^:0|0:$/g, zeros ? '0:0' : '0')

        ,shortIP = longIP
            .replace(/(\b0(:0)*)(?!.*\1:0)/,':')
            .replace(/::+/,'::');

    return /^(:[\da-f]{1,4}){8}$/i.test(':'+longIP) && [longIP, shortIP];
}

Explanation:

To calculate the long version of the IPv6 address:

8 - str.split(/:+/).length % 9 - calculate how many zeros we need to insert. They are 8 - the number of the hex values. Here % 9 is a guard so it will never be a negative number.

replace('::', ':0'.repeat(zeros || 1) + ':') - replace the "::" with colon separated zeros. If there are no zeros to add it still adds one so the address won't be valid in the end

replace(/^:0|0:$/g, zeros ? '0:0' : '0') - this deals with the special case when the address starts or ends with "::" as the split function adds 1 to the number of hex values (::1 -> ["", "1"])

That's it! Now let's calculate the short form:

replace(/(\b0(:0)*)(?!.*\1:0)/,':') - replace longest row of zeros with colon(s) (It doesn't matter how many).

replace(/::+/,'::') - remove the extra colons if any

return /^(:[\da-f]{1,4}){8}$/i.test(':'+longIP) && [longIP, shortIP]; - test if the long version is valid IPv6 and return both versions or false if the test fails.

Tests in Firefox:

>>> f('1080:0:0:0:8:800:200C:417A')
["1080:0:0:0:8:800:200C:417A", "1080::8:800:200C:417A"]
>>> f('FF01::101')
["FF01:0:0:0:0:0:0:101", "FF01::101"]
>>> f('0:0:0:0:0:0:0:1')
["0:0:0:0:0:0:0:1", "::1"]
>>> f('::')
["0:0:0:0:0:0:0:0", "::"]
>>> f('1:0:0:2:0:0:0:3')
["1:0:0:2:0:0:0:3", "1:0:0:2::3"]
>>> f('1:0:0:8:8:0:0:3')
["1:0:0:8:8:0:0:3", "1::8:8:0:0:3"]
>>> f('1:2:3:4:5:6:7:8')
["1:2:3:4:5:6:7:8", "1:2:3:4:5:6:7:8"]
>>> f('ABCD:1234')
false
>>> f('ABCDE::1234')
false
>>> f('1:2:3:4:5:6:7:8:9')
false
>>> f(':::1')
false
>>> f('1:2:3:4::a:b:c:d')
false
>>> f('codegolf puzzle')
false

Javascript (E6) 246 305 284 292 319

Heavily revised Special case for :: specifically handled, compress phase avoids the for loop (but not very shorter indeed) I'm sure that the final compress phase can be made shorter. Not now anyway

F=i=>(c=':',d=c+c,z=':0'.repeat(9-i.split(c,9).length)+c,i=i==d?0+z+0:i[R='replace'](/^::/,0+z)[R](/::$/,z+0)[R](d,z>c?z:d),/^(:[\da-f]{1,4}){8}:$/i.test(k=c+i+c)&&[i,k[R]((k.match(/:(0:)+/g)||[]).sort().pop(),d)[R](/^:([^:])|([^:]):$/g,'$1$2')])

Thanks to nderscore

As a program

Input and output using js popup, basically: p=prompt,p(F(p())) Rewriting with popup and without the function definition, the char count should be under 260

Ungolfed and commented a bit

F = i => (
  c = ':',
  d = c+c,
  z = ':0'.repeat(9-i.split(c,9).length) + c, 
  i = i == d ? 0+z+0 /* special case '::' */
    : i.replace(/^::/,0+z) /* special case '::...' */
       .replace(/::$/,z+0) /* special case '...::' */
       .replace(d, z > c ? z : d), /* here, if z==c, not valid: too much colons */
  /^(:[\da-f]{1,4}){8}:$/i.test(k = c+i+c) /* Check if valid */
  && [
   i, 
   k.replace((k.match(/:(0:)+/g)||[]).sort().pop(),d) /* find longest 0: sequence and replace it */
    .replace(/^:([^:])|([^:]):$/g,'$1$2') /* cut leading and trailing colons */
  ]
)

Test In console

i=['1080:0:0:0:8:800:200C:417A'
, '::1:2:3:4:5:6:7', '1:2:3:4:5:6:7::'
, '1:2:3:4::5:6:7:8'
, ':1:2:3:4:5:6:7', '1:2:3:4:5:6:7:'
, 'FF01::101', '0:0:0:0:0:0:0:1'
, '::', '1::', '::1', ':::1', '1:::'
, '1:0:0:2:0:0:0:3', '1:0:0:0:2:0:0:3', '1::8:0:0:0:3'
, '1:2:3:4:5:6:7:8'
, 'ABCD:1234', 'ABCDE::1234', ':::', '::::::::::'
, '1:2:3:4:5:6:7:8:9', '::::1', 'codegolf puzzle'];
i.map(x=>x+' => '+F(x)).join('\n')

Test output

"1080:0:0:0:8:800:200C:417A => 1080:0:0:0:8:800:200C:417A,1080::8:800:200C:417A
::1:2:3:4:5:6:7 => 0:1:2:3:4:5:6:7,::1:2:3:4:5:6:7
1:2:3:4:5:6:7:: => 1:2:3:4:5:6:7:0,1:2:3:4:5:6:7::
1:2:3:4::5:6:7:8 => false
:1:2:3:4:5:6:7 => false
1:2:3:4:5:6:7: => false
FF01::101 => FF01:0:0:0:0:0:0:101,FF01::101
0:0:0:0:0:0:0:1 => 0:0:0:0:0:0:0:1,::1
:: => 0:0:0:0:0:0:0:0,::
1:: => 1:0:0:0:0:0:0:0,1::
::1 => 0:0:0:0:0:0:0:1,::1
:::1 => false
1::: => false
1:0:0:2:0:0:0:3 => 1:0:0:2:0:0:0:3,1:0:0:2::3
1:0:0:0:2:0:0:3 => 1:0:0:0:2:0:0:3,1::2:0:0:3
1::8:0:0:0:3 => 1:0:0:8:0:0:0:3,1:0:0:8::3
1:2:3:4:5:6:7:8 => 1:2:3:4:5:6:7:8,1:2:3:4:5:6:7:8
ABCD:1234 => false
ABCDE::1234 => false
::: => false
:::::::::: => false
1:2:3:4:5:6:7:8:9 => false
::::1 => false
codegolf puzzle => false"   

sed, 276

I have 275 bytes in ipshorten.sed, plus 1 byte for the -r switch in sed -rf to use extended regular expressions. I used OpenBSD sed(1).

Usage: echo ::2:3:4:a:b:c:d | sed -rf ipshorten.sed

s/^/:/
/^(:[0-9A-Fa-f]{0,4})*$/!d
s/:0*([^:])/:\1/g
s/://
s/::/:=/
s/(.:=)(.)/\10:\2/
s/^:=/0&/
s/=$/&0/
:E
/(.*:){7}/!{/=/!d
s//=0:/
bE
}
s/=//
/^:|::|:$|(.*:){8}/d
p
s/.*/:&:/
s/:((0:)+)/:<\1>/g
:C
s/0:>/>0:/g
/<0/{s/<>//g
bC
}
s/<>(0:)+/:/
s/<>//g
/^::/!s/://
/::$/!s/:$//

I use 22 regular expressions, as sed can't compare numbers or make arrays. For each line of input, sed runs the commands and prints the line. During testing, I put several lines of alleged IP addresses in a file, and fed this file to sed. A reference to extended regular expressions is in re_format(7).

1. s/^/:/ adds an extra colon to the beginning of the line. I use this extra colon to golf the next two commands.
2. /^(:[0-9A-Fa-f]{0,4})*$/!d checks if the whole line matches zero or more groups of colons followed by zero to four hexadecimal digits. ! negates the check, so d deletes lines with too big hexadecimal numbers or with invalid characters. When d deletes a line, sed runs no more commands on this line.
3. s/:0*([^:])/:\1/g deletes leading 0s from each number. It would change :0000:0000: to :0:0:. I must do this because my contraction loop only works with single-digit 0s.
4. s/:// deletes the extra colon. It deletes only the first colon.
5. s/::/:=/ changes the first :: to :=. This is so later commands can match = rather than ::, and so = does not count as a colon. If there is no ::, this substitution safely does nothing.
   • Now :: must make at least one 0, but there are three different cases for placing this 0.
6. s/(.:=)(.)/\10:\2/ is the first case. If :: was between two other characters, then := becomes :=0:. This is the only case that adds a colon.
7. s/^:=/0&/ is the second case. If :: was at beginning of line, then put 0 there.
8. s/=$/&0/ is the third case, for :: at end of line.
9. :E is the label for the expansion loop.
10. /(.*:){7}/!{/=/!d begins a conditional block if the line has fewer than 7 colons. /=/!d deletes lines that had no :: and not enough colons.
11. s//=0:/ adds one colon. Empty // repeats the last regular expression, so this is really s/=/=0:/.
12. bE branches to :E to continue the loop.
13. } closes the block. Now the line has at least seven colons.
14. s/=// deletes =.
15. /^:|::|:$|(.*:){8}/d is a final check after expansion. It deletes lines with a leading colon, an extra :: that was not expanded, a trailing colon, or eight or more colons.
16. p prints the line, which is an IP address in long form.
17. s/.*/:&:/ wraps the address in extra colons.
    • The next task is to find the longest group of 0s, like :0:0:0:, and contract it into ::.
18. s/:((0:)+)/:<\1>/g eats each group of 0s, so :0:0:0: would become :<0:0:0:>.
19. :C is the label for the contraction loop.
20. s/0:>/>0:/g moves one 0 from each mouth, so :<0:0:0:> would become :<0:0:>0:.
21. /<0/{s/<>//g opens a conditional block if any mouth is not empty. s/<>//g deletes all empty mouths, because those groups are too short.
22. bC continues the contraction loop.
23. } closes the block. Now any mouth is empty and marks the longest group of 0s.
24. s/<>(0:)+/:/ contracts the longest group, so :<>0:0:0: would become ::. In a tie, it picks the empty mouth on the left.
25. s/<>//g deletes any other empty mouths.
26. /^::/!s/:// deletes the first extra colon unless it is part of ::.
27. /::$/!s/:$// does so for the last extra colon. Then sed prints the IP address in short form.

Perl - 204 176 190 191 197

(202 chars + 2 for -p flag)

$_=uc;(9-split/:/)||/^:|:$/||last;s/^::/0::/;s/::$/::0/;s|::|':0'x(9-split/:/).':'|e;/::|^:|:$|\w{5}|[^A-F0-:].*\n/||(8-split/:/)and last;s/\b0*(?!\b)//g;print;s/\b((0:)*0)\b(?!.*\1:0\b)/::/;s/::::?/::/

Example:

$ perl -p ipv6.pl <<< 1:0:2:0::3
1:0:2:0:0:0:0:3
1:0:2::3
$ perl -p ipv6.pl <<< somethinginvalid
$ perl -p ipv6.pl <<< 1:2:0:4:0:6::8
1:2:0:4:0:6:0:8
1:2::4:0:6:0:8

Explanation:

# -p reads a line from stdin and stores in $_
#
# Convert to uppercase
$_ = uc;

# Detect the annoying case @kernigh pointed out
(9 - split /:/) || /^:|:$/ || last;

# Fix :: hanging on the beginning or the end of the string
s/^::/0::/;
s/::$/::0/;

# Replace :: with the appropriate number of 0 groups
s|::|':0' x (9 - split /:/) . ':'|e;

# Silently exit if found an extra ::, a hanging :, a 5-char group, an invalid
# character, or there's not 8 groups
/::|^:|:$|\w{5}|[^A-F0-:].*\n/ || (8 - split /:/) and last;

# Remove leading zeros from groups
s/\b0*(?!\b)//g;

# Output the ungolfed form
print;

# Find the longest sequence of 0 groups (a sequence not followed by something
# and a longer sequence) and replace with ::
# This doesn't replace the colons around the sequence because those are optional
# thus we are left with 4 or 3 colons in a row
s/\b((0:)*0)\b(?!.*\1:0\b)/::/;

# Fix the colons after previous transformation
s/::::?/::/

# -p then prints the golfed form of the address

Python 3: 387 characters

Even works with improperly shortened input.

$ echo '1::2:0:0:0:3' | python3 ipv6.py 
1:0:0:2:0:0:0:3
1:0:0:2::3

The double replace of ':::' with '::' feels really bad but not sure how to cleanly deal with the longest string of 0's when it abuts one or both ends.

c=':'
p=print
try:
 B=[int(x,16)if x else''for x in input().split(c)];L=len(B)
 if any(B)-1:B=[''];L=1
 if L!=8:s=B.index('');B[s:s+1]=[0]*(9-L)
 for b in B:assert-1<b<2**16
 H=[format(x,'X')for x in B];o=c.join(H);p(o);n=''.join(str(h=='0')[0]for h in H)
 for i in range(8,0,-1):
  s=n.find('T'*i)
  if s>=0:H[s:s+i]=[c*2];p(c.join(H).replace(c*3,c*2).replace(c*3,c*2));q
 p(o)
except:0

Replace the final pass with raise to see how it's crashing protecting against malformed input.

$ cat ipv6-test.sh 
echo '1080:0:0:0:8:800:200C:417A' | python3 ipv6.py
echo '1:2:3:4:5:6:7:8' | python3 ipv6.py
echo 'FF01::101' | python3 ipv6.py
echo '0:0:0:0:0:0:0:1' | python3 ipv6.py
echo '0:0:0:0:1:0:0:0' | python3 ipv6.py
echo '1:0:0:0:0:0:0:0' | python3 ipv6.py
echo '::' | python3 ipv6.py
echo '1:0:0:2:0:0:0:3' | python3 ipv6.py
echo '1::2:0:0:0:3' | python3 ipv6.py
echo '1:0:0:8:8:0:0:3' | python3 ipv6.py
echo 'ABCD:1234' | python3 ipv6.py
echo 'ABCDE::1234' | python3 ipv6.py
echo '1:2:3:4:5:6:7:8:9' | python3 ipv6.py
echo ':::1' | python3 ipv6.py
echo 'codegolf puzzle' | python3 ipv6.py
$ ./ipv6-test.sh 
1080:0:0:0:8:800:200C:417A
1080::8:800:200C:417A

1:2:3:4:5:6:7:8
1:2:3:4:5:6:7:8

FF01:0:0:0:0:0:0:101
FF01::101

0:0:0:0:0:0:0:1
::1

0:0:0:0:1:0:0:0
::1:0:0:0

1:0:0:0:0:0:0:0
1::


0:0:0:0:0:0:0:0
::

1:0:0:2:0:0:0:3
1:0:0:2::3

1:0:0:2:0:0:0:3
1:0:0:2::3

1:0:0:8:8:0:0:3
1::8:8:0:0:3